anchor.diff:  
               let POLYNOMIAL_NEG_CONV = 
                   fun tm -> 
  -                    let l, r = Choice.get <| dest_comb tm
  -                    if l <> neg_tm
  -                    then failwith "POLYNOMIAL_NEG_CONV"
  -                    else 
  -                        let th1 = INST [r, x_tm] nthm_1
  -                        TRANS th1 
  -                            (POLYNOMIAL_MONOMIAL_MUL_CONV
  -                                    (Choice.get <| rand(concl <| Choice.get th1)))
  +                    choice {
  +                        let! l, r = dest_comb tm
  +                        if l <> neg_tm
  +                        then 
  +                            return! failwith "POLYNOMIAL_NEG_CONV"
  +                        else 
  +                            let th1 = INST [r, x_tm] nthm_1
  +                            let! tm1' = Choice.bind (rand << concl) th1
  +                            return! TRANS th1 (POLYNOMIAL_MONOMIAL_MUL_CONV tm1')
  +                    }
   
               (* ------------------------------------------------------------------------- *)
               (* Subtraction.                                                              *)
  
positive.code: 
              let MONOMIAL_MUL_CONV = 
                  let powvar tm = 
                      if is_semiring_constant tm
                      then one_tm
                      else 
                          try 
                              let lop, r = Choice.get <| dest_comb tm
                              let op, l = Choice.get <| dest_comb lop
                              if op = pow_tm && is_numeral r
                              then l
                              else failwith ""
                          with
                          | Failure _ -> tm
                  let vorder x y = 
                      if x = y
                      then 0
                      elif x = one_tm
                      then -1
                      elif y = one_tm
                      then 1
                      elif variable_order x y
                      then -1
                      else 1
                  let rec MONOMIAL_MUL tm l r = 
                      try 
                          let lx, ly = dest_mul l
                          let vl = powvar lx
                          try 
                              let rx, ry = dest_mul r
                              let vr = powvar rx
                              let ord = vorder vl vr
                              if ord = 0
                              then 
                                  let th1 = 
                                      INST [lx, lx_tm; ly, ly_tm; rx, rx_tm; ry, ry_tm] pthm_15
                                  let tm1, tm2 = 
                                      Choice.get <| dest_comb(Choice.get <| rand(concl <| Choice.get th1))
                                  let tm3, tm4 = Choice.get <| dest_comb tm1
                                  let th2 = 
                                      AP_THM 
                                          (AP_TERM tm3 
                                                  (POWVAR_MUL_CONV tm4)) 
                                          tm2
                                  let th3 = TRANS th1 th2
                                  let tm5, tm6 = 
                                      Choice.get <| dest_comb(Choice.get <| rand(concl <| Choice.get th3))
                                  let tm7, tm8 = Choice.get <| dest_comb tm6
                                  let th4 = 
                                      MONOMIAL_MUL tm6 (Choice.get <| rand tm7) tm8
                                  TRANS th3 (AP_TERM tm5 th4)
                              else 
                                  let th0 = 
                                      if ord < 0
                                      then pthm_16
                                      else pthm_17
                                  let th1 = 
                                      INST [lx, lx_tm; ly, ly_tm; rx, rx_tm; ry, ry_tm] th0
                                  let tm1, tm2 = 
                                      Choice.get <| dest_comb(Choice.get <| rand(concl <| Choice.get th1))
                                  let tm3, tm4 = Choice.get <| dest_comb tm2
                                  TRANS th1 
                                      (AP_TERM tm1 
                                              (MONOMIAL_MUL tm2 
                                                  (Choice.get <| rand tm3) tm4))
                          with
                          | Failure _ -> 
                              let vr = powvar r
                              let ord = vorder vl vr
                              if ord = 0
                              then 
                                  let th1 = 
                                      INST [lx, lx_tm; ly, ly_tm; r, rx_tm] pthm_18
                                  let tm1, tm2 = 
                                      Choice.get <| dest_comb(Choice.get <| rand(concl <| Choice.get th1))
                                  let tm3, tm4 = Choice.get <| dest_comb tm1
                                  let th2 = 
                                      AP_THM 
                                          (AP_TERM tm3 
                                                  (POWVAR_MUL_CONV tm4)) 
                                          tm2
                                  TRANS th1 th2
                              elif ord < 0
                              then 
                                  let th1 = 
                                      INST [lx, lx_tm; ly, ly_tm; r, rx_tm] pthm_19
                                  let tm1, tm2 = 
                                      Choice.get <| dest_comb(Choice.get <| rand(concl <| Choice.get th1))
                                  let tm3, tm4 = Choice.get <| dest_comb tm2
                                  TRANS th1 
                                      (AP_TERM tm1 
                                              (MONOMIAL_MUL tm2 
                                                  (Choice.get <| rand tm3) tm4))
                              else 
                                  INST [l, lx_tm; r, rx_tm] pthm_20
                      with
                      | Failure _ -> 
                          let vl = powvar l
                          try 
                              let rx, ry = dest_mul r
                              let vr = powvar rx
                              let ord = vorder vl vr
                              if ord = 0
                              then 
                                  let th1 = 
                                      INST [l, lx_tm; rx, rx_tm; ry, ry_tm] pthm_21
                                  let tm1, tm2 = 
                                      Choice.get <| dest_comb(Choice.get <| rand(concl <| Choice.get th1))
                                  let tm3, tm4 = Choice.get <| dest_comb tm1
                                  TRANS th1 
                                      (AP_THM 
                                              (AP_TERM tm3 
                                                  (POWVAR_MUL_CONV tm4)) 
                                              tm2)
                              elif ord > 0
                              then 
                                  let th1 = 
                                      INST [l, lx_tm; rx, rx_tm; ry, ry_tm] pthm_22
                                  let tm1, tm2 = 
                                      Choice.get <| dest_comb(Choice.get <| rand(concl <| Choice.get th1))
                                  let tm3, tm4 = Choice.get <| dest_comb tm2
                                  TRANS th1 
                                      (AP_TERM tm1 
                                              (MONOMIAL_MUL tm2 
                                                  (Choice.get <| rand tm3) tm4))
                              else REFL tm
                          with
                          | Failure _ -> 
                              let vr = powvar r
                              let ord = vorder vl vr
                              if ord = 0
                              then POWVAR_MUL_CONV tm
                              elif ord > 0
                              then 
                                  INST [l, lx_tm; r, rx_tm] pthm_20
                              else REFL tm
                  fun tm -> 
                      let l, r = dest_mul tm
                      MONOMIAL_DEONE(MONOMIAL_MUL tm l r)
  
              (* ------------------------------------------------------------------------- *)
              (* Multiplication by monomial of a polynomial.                               *)
  
negative.code: 
              let POLYNOMIAL_MUL_CONV = 
                  let rec PMUL tm = 
                      choice {
                          let! l, r = dest_mul tm
                          if not(is_add l) then 
                              return! POLYNOMIAL_MONOMIAL_MUL_CONV tm
                          elif not(is_add r) then 
                              let th1 = 
                                  INST [l, a_tm;
                                        r, b_tm] pthm_09
                              let! tm1' = Choice.bind (rand << concl) th1
                              return! TRANS th1 (POLYNOMIAL_MONOMIAL_MUL_CONV tm1')
                          else 
                              let! a, b = dest_add l
                              let th1 = 
                                  INST [a, a_tm;
                                        b, b_tm;
                                        r, c_tm] pthm_10
                              let! tm1' = Choice.bind (rand << concl) th1
                              let! tm1, tm2 = dest_comb tm1'
                              let! tm3, tm4 = dest_comb tm1
                              let th2 = AP_TERM tm3 (POLYNOMIAL_MONOMIAL_MUL_CONV tm4)
                              let th3 = TRANS th1 (MK_COMB(th2, PMUL tm2))
                              let! tm2' = Choice.bind (rand << concl) th3
                              return! TRANS th3 (POLYNOMIAL_ADD_CONV tm2')
                      }
  
                  fun tm -> 
                      choice {
                          let! l, r = dest_mul tm
                          if l = zero_tm then 
                              return! INST [r, a_tm] pthm_11
                          elif r = zero_tm then 
                              return! INST [l, a_tm] pthm_12
                          elif l = one_tm then 
                              return! INST [r, a_tm] pthm_13
                          elif r = one_tm then 
                              return! INST [l, a_tm] pthm_14
                          else 
                              return! PMUL tm
                      }
  
              (* ------------------------------------------------------------------------- *)
              (* Power of polynomial (optimized for the monomial and trivial cases).       *)
  