anchor.diff:  
               let POLYNOMIAL_MONOMIAL_MUL_CONV = 
                   let rec PMM_CONV tm = 
  -                    let l, r = dest_mul tm
  -                    try 
  -                        let y, z = dest_add r
  +                    let lr = dest_mul tm
  +                    choice { 
  +                        let! l, r = lr
  +                        let! y, z = dest_add r
                           let th1 = 
                               INST [l, x_tm; y, y_tm; z, z_tm] pthm_37
  -                        let tm1, tm2 = Choice.get <| dest_comb(Choice.get <| rand(concl <| Choice.get th1))
  -                        let tm3, tm4 = Choice.get <| dest_comb tm1
  -                        let th2 = 
  -                            MK_COMB
  -                                (AP_TERM tm3 (MONOMIAL_MUL_CONV tm4), 
  -                                    PMM_CONV tm2)
  -                        TRANS th1 th2
  -                    with
  -                    | Failure _ -> MONOMIAL_MUL_CONV tm
  +                        let! tm1' = Choice.bind (rand << concl) th1
  +                        let! tm1, tm2 = dest_comb tm1'
  +                        let! tm3, tm4 = dest_comb tm1
  +                        let th2 = MK_COMB (AP_TERM tm3 (MONOMIAL_MUL_CONV tm4), PMM_CONV tm2)
  +                        return! TRANS th1 th2
  +                    }
  +                    |> Choice.bindError (fun _ -> 
  +                        choice {
  +                            let! l, r = lr
  +                            return! MONOMIAL_MUL_CONV tm
  +                        })
                   PMM_CONV
   
               (* ------------------------------------------------------------------------- *)
  
positive.code:     let true_tm = Choice.map concl TRUTH
  
      fun sth rth (is_semiring_constant, SEMIRING_ADD_CONV, SEMIRING_MUL_CONV, SEMIRING_POW_CONV) -> 
          let pthm_01, pthm_02, pthm_03, pthm_04, pthm_05, pthm_06, pthm_07, pthm_08, pthm_09, pthm_10, pthm_11, pthm_12, pthm_13, pthm_14, pthm_15, pthm_16, pthm_17, pthm_18, pthm_19, pthm_20, pthm_21, pthm_22, pthm_23, pthm_24, pthm_25, pthm_26, pthm_27, pthm_28, pthm_29, pthm_30, pthm_31, pthm_32, pthm_33, pthm_34, pthm_35, pthm_36, pthm_37, pthm_38 =
              let pthFuncs = CONJUNCTS(MATCH_MP SEMIRING_PTHS sth)
              match pthFuncs with
              | [pthm_01; pthm_02; pthm_03; pthm_04; pthm_05; pthm_06; pthm_07; pthm_08; pthm_09; pthm_10; pthm_11; pthm_12; pthm_13; pthm_14; pthm_15; pthm_16; pthm_17; pthm_18; pthm_19; pthm_20; pthm_21; pthm_22; pthm_23; pthm_24; pthm_25; pthm_26; pthm_27; pthm_28; pthm_29; pthm_30; pthm_31; pthm_32; pthm_33; pthm_34; pthm_35; pthm_36; pthm_37; pthm_38] ->
                  pthm_01, pthm_02, pthm_03, pthm_04, pthm_05, pthm_06, pthm_07, pthm_08, pthm_09, pthm_10, pthm_11, pthm_12, pthm_13, pthm_14, pthm_15, pthm_16, pthm_17, pthm_18, pthm_19, pthm_20, pthm_21, pthm_22, pthm_23, pthm_24, pthm_25, pthm_26, pthm_27, pthm_28, pthm_29, pthm_30, pthm_31, pthm_32, pthm_33, pthm_34, pthm_35, pthm_36, pthm_37, pthm_38
              | _ -> failwith "pthFuncs: Unhandled case."
          let add_tm = Choice.get <| rator(Choice.get <| rator(Choice.get <| lhand(concl <| Choice.get pthm_07)))
          let mul_tm = Choice.get <| rator(Choice.get <| rator(Choice.get <| lhand(concl <| Choice.get pthm_13)))
          let pow_tm = Choice.get <| rator(Choice.get <| rator(Choice.get <| rand(concl <| Choice.get pthm_32)))
          let zero_tm = Choice.get <| rand(concl <| Choice.get pthm_06)
          let one_tm = Choice.get <| rand(Choice.get <| lhand(concl <| Choice.get pthm_14))
          let ty = Choice.get <| type_of(Choice.get <| rand(concl <| Choice.get pthm_01))
          let p_tm = (parse_term @"p:num")
          let q_tm = (parse_term @"q:num")
          let zeron_tm = (parse_term @"0")
  
negative.code:         let x_tm = mk_var("x", ty)
          let y_tm = mk_var("y", ty)
          let z_tm = mk_var("z", ty)
          let dest_add = dest_binop add_tm
          let dest_mul = dest_binop mul_tm
  
          let dest_pow tm = 
              choice {
                  let! l, r = dest_binop pow_tm tm
                  if is_numeral r then 
                      return l, r
                  else 
                      return! Choice.failwith "dest_pow"
              }
  
          let is_add = is_binop add_tm
          let is_mul = is_binop mul_tm
  
          let! nthm_1, nthm_2, sub_tm, neg_tm, dest_sub, is_sub = 
              choice {
                  let! true_tm = true_tm
                  let! rtm = Choice.map concl rth
                  if rtm = true_tm then 
                      return rth, rth, true_tm, true_tm, (fun t -> t, t), K false
                  else 
                      let nthm_1 = SPEC x_tm (CONJUNCT1 rth)
                      let nthm_2 = SPECL [x_tm; y_tm] (CONJUNCT2 rth)
                      let! tm1 = (Choice.bind rator << Choice.bind lhand << Choice.map concl) nthm_2
                      let! sub_tm = rator tm1
                      let! tm2 = Choice.bind (lhand << concl) nthm_1
                      let! neg_tm = rator tm2
                      let dest_sub = Choice.get << dest_binop sub_tm
                      let is_sub = is_binop sub_tm
                      return (nthm_1, nthm_2, sub_tm, neg_tm, dest_sub, is_sub)
              }
          
          // It's weird to return a function value like this
          return
            fun variable_order -> 
  
              (* ------------------------------------------------------------------------- *)
              (* Conversion for "x^n * x^m", with either x^n = x and/or x^m = x possible.  *)
  