anchor.diff:          let mul_tm = (parse_term @"(int_mul)")
           let add_tm = (parse_term @"(int_add)")
           let neg_tm = (parse_term @"(int_neg)")
  -        let dest_mul = Choice.get << dest_binop mul_tm
  -        let dest_add = Choice.get << dest_binop add_tm
  -        let mk_mul = fun x -> Choice.get << mk_binop mul_tm x
  -        let mk_add = fun x -> Choice.get << mk_binop add_tm x
  +        let dest_mul = dest_binop mul_tm
  +        let dest_add = dest_binop add_tm
  +        let mk_mul = mk_binop mul_tm
  +        let mk_add = mk_binop add_tm
  +
           let scrub_var v m = 
  -            let ps = striplist (Some << dest_mul) m
  -            let ps' = subtract ps [v]
  -            if ps' = []
  -            then one_tm
  -            else end_itlist mk_mul ps'
  +            choice {
  +                let ps = striplist (Choice.toOption << dest_mul) m
  +                let ps' = subtract ps [v]
  +                if ps' = [] then 
  +                    return one_tm
  +                else 
  +                    return! Choice.List.reduceBack mk_mul ps'
  +            }
  +
           let find_multipliers v mons = 
  -            let mons1 = filter (fun m -> free_in v m) mons
  -            let mons2 = map (scrub_var v) mons1
  -            if mons2 = []
  -            then zero_tm
  -            else end_itlist mk_add mons2
  +            choice {
  +                let mons1 = filter (fun m -> free_in v m) mons
  +                let! mons2 = Choice.List.map (scrub_var v) mons1
  +                if mons2 = [] then 
  +                    return zero_tm
  +                else 
  +                    return! Choice.List.reduceBack mk_add mons2
  +            }
  +
           fun vars tm -> 
  -            let cmons, vmons = 
  -                partition (fun m -> intersect (frees m) vars = []) 
  -                    (striplist (Some << dest_add) tm)
  -            let cofactors = map (fun v -> find_multipliers v vmons) vars
  -            let cnc = 
  -                if cmons = []
  -                then zero_tm
  -                else Choice.get <| mk_comb(neg_tm, end_itlist mk_add cmons)
  -            cofactors, cnc
  +            choice {
  +                let cmons, vmons = partition (fun m -> intersect (frees m) vars = []) (striplist (Choice.toOption << dest_add) tm)
  +                let! cofactors = Choice.List.map (fun v -> find_multipliers v vmons) vars
  +                let! cnc = 
  +                    choice {
  +                        if cmons = [] then 
  +                            return zero_tm
  +                        else
  +                            let! tm1 = Choice.List.reduceBack mk_add cmons 
  +                            return! mk_comb(neg_tm, tm1)
  +                    }
  +
  +                return cofactors, cnc
  +            }
  +
       let isolate_variables evs ps eq = 
  -        let vars = filter (fun v -> vfree_in v eq) evs
  -        let qs, p = isolate_monomials vars eq
  -        let rs = filter (fun t -> Choice.get <| type_of t = int_ty) (qs @ ps)
  -        let rs = int_ideal_cofactors rs p
  -        eq, zip (fst(chop_list (length qs) rs)) vars
  -
  -    let subst_in_poly i p = Choice.get <| rhs(concl <| Choice.get(INT_POLY_CONV(Choice.get <| vsubst i p)))
  +        choice {
  +            let vars = filter (fun v -> vfree_in v eq) evs
  +            let! qs, p = isolate_monomials vars eq
  +            let! rs = Choice.List.filter (fun t -> 
  +                        choice {
  +                            let! ty = type_of t
  +                            return ty = int_ty
  +                        }) (qs @ ps)
  +
  +            let! rs = int_ideal_cofactors rs p
  +            return eq, zip (fst(chop_list (length qs) rs)) vars
  +        }
  +
  +    let subst_in_poly i p = 
  +        choice {
  +            let! tm1 = vsubst i p
  +            let! tm2 = INT_POLY_CONV tm1
  +            return! rhs(concl <| tm2)
  +        }
  +
       let rec solve_idealism evs ps eqs = 
  -        if evs = []
  -        then []
  -        else 
  -            let eq, cfs = 
  -                tryfind (Some << isolate_variables evs ps) eqs
  -                |> Option.getOrFailWith "tryfind"
  -                    
  -            let evs' = subtract evs (map snd cfs)
  -            let eqs' = map (subst_in_poly cfs) (subtract eqs [eq])
  -            cfs @ solve_idealism evs' ps eqs'
  +        choice {
  +            if evs = [] then 
  +                return []
  +            else 
  +                let eq, cfs = tryfind (Choice.toOption << isolate_variables evs ps) eqs |> Option.getOrFailWith "tryfind"
  +                let evs' = subtract evs (map snd cfs)
  +                let! eqs' = Choice.List.map (subst_in_poly cfs) (subtract eqs [eq])
  +                let! cfs' = solve_idealism evs' ps eqs'
  +                return cfs @ cfs'
  +        }
  +    
       let rec GENVAR_EXISTS_CONV tm = 
  -        if not(is_exists tm)
  -        then REFL tm
  -        else 
  -            let ev, bod = Choice.get <| dest_exists tm
  -            let gv = genvar(Choice.get <| type_of ev)
  -            (GEN_ALPHA_CONV gv
  -             |> THENC <| BINDER_CONV GENVAR_EXISTS_CONV) tm
  +        choice {
  +            if not(is_exists tm) then 
  +                return! REFL tm
  +            else 
  +                let! ev, bod = dest_exists tm
  +                let! gv = Choice.map genvar (type_of ev)
  +                return! 
  +                    (GEN_ALPHA_CONV gv
  +                     |> THENC <| BINDER_CONV GENVAR_EXISTS_CONV) tm
  +        }
  +
       let EXISTS_POLY_TAC(asl, w as gl) = 
  -        let evs, bod = strip_exists w
  -        let ps = 
  -            mapfilter 
  -                (Choice.toOption << check(fun t -> Choice.get <| type_of t = int_ty) << Choice.get << lhs << concl << Choice.get << snd) asl
  -        let cfs = solve_idealism evs ps (map (Choice.get << lhs) (conjuncts bod))
  -        (MAP_EVERY EXISTS_TAC (map (fun v -> rev_assocd v cfs zero_tm) evs)
  -         |> THEN <| REPEAT(POP_ASSUM MP_TAC)
  -         |> THEN <| CONV_TAC INT_RING) gl
  +        choice {
  +            let evs, bod = strip_exists w
  +            let ps = 
  +                mapfilter 
  +                    (Choice.toOption << check(fun t -> Choice.get <| type_of t = int_ty) << Choice.get << lhs << concl << Choice.get << snd) asl
  +            
  +            let! tms = Choice.List.map lhs (conjuncts bod)
  +            let! cfs = solve_idealism evs ps tms
  +            return!
  +                (MAP_EVERY EXISTS_TAC (map (fun v -> rev_assocd v cfs zero_tm) evs)
  +                 |> THEN <| REPEAT(POP_ASSUM MP_TAC)
  +                 |> THEN <| CONV_TAC INT_RING) gl
  +         }
   
       let SCRUB_NEQ_TAC = 
           MATCH_MP_TAC 
  
positive.code:             let mons = striplist (Choice.toOption << dest_binary "int_add") t
              mem v mons && forall (fun m -> v = m || not(free_in v m)) mons
          fun vars tm -> 
              let th = INT_POLYEQ_CONV tm
              let th' = (SYM_CONV
                         |> THENC <| INT_POLYEQ_CONV) tm
              let v, th1 = 
                  try 
                      Option.get <| find (fun v -> is_defined v (Choice.get <| lhand(Choice.get <| rand(concl <| Choice.get th)))) vars, 
                      th'
                  with
                  | Failure _ -> 
                      Option.get <| find (fun v -> is_defined v (Choice.get <| lhand(Choice.get <| rand(concl <| Choice.get th')))) vars, 
                      th
              let th2 = 
                  TRANS th1 (SPECL [Choice.get <| lhs(Choice.get <| rand(concl <| Choice.get th1))
                                    v] <| pth())
              CONV_RULE (RAND_CONV(RAND_CONV INT_POLY_CONV)) th2
  
      let UNWIND_POLYS_CONV tm = 
          let vars, bod = strip_exists tm
          let cjs = conjuncts bod
          let th1 = tryfind (Choice.toOption << ISOLATE_VARIABLE vars) cjs |> Option.toChoiceWithError "tryfind"
          let eq = Choice.get <| lhand(concl <| Choice.get th1)
          let bod' = list_mk_conj(eq :: (subtract cjs [eq]))
          let th2 = CONJ_ACI_RULE(Choice.get <| mk_eq(bod, bod'))
          let th3 = TRANS th2 (MK_CONJ th1 (REFL(Choice.get <| rand(Choice.get <| rand(concl <| Choice.get th2)))))
          let v = Choice.get <| lhs(Choice.get <| lhand(Choice.get <| rand(concl <| Choice.get th3)))
          let vars' = (subtract vars [v]) @ [v]
          let th4 = CONV_RULE (RAND_CONV(REWR_CONV UNWIND_THM2)) (MK_EXISTS v th3)
          let IMP_RULE v v' = 
              DISCH_ALL
                  (itlist SIMPLE_CHOOSE v (itlist SIMPLE_EXISTS v' (ASSUME bod)))
          let th5 = IMP_ANTISYM_RULE (IMP_RULE vars vars') (IMP_RULE vars' vars)
          TRANS th5 (itlist MK_EXISTS (subtract vars [v]) th4)
  
      let zero_tm = (parse_term @"&0")
      let one_tm = (parse_term @"&1")
  
negative.code:             let! r' = dest_intconst r
              return! CONJUNCT2(INT_DIVMOD_CONV l' r')
          }
          |> Choice.mapError (fun e -> nestedFailure e "INT_MOD_CONV"));;
  
  /// Performs one arithmetic or relational operation on integer literals of type :int.
  let INT_RED_CONV = 
  