anchor.diff:  
   /// Tactic to introduce an abbreviation.
   let ABBREV_TAC tm : tactic =
  -    let cvs, t = Choice.get <| dest_eq tm
  -    let v, vs = strip_comb cvs
  -    let rs = list_mk_abs(vs, t)
  -    let eq = Choice.get <| mk_eq(rs, v)
  -    let th1 = 
  -        itlist (fun v th -> CONV_RULE (LAND_CONV BETA_CONV) (AP_THM th v)) 
  -            (rev vs) (ASSUME eq)
  -    let th2 = SIMPLE_CHOOSE v (SIMPLE_EXISTS v (GENL vs th1))
  -    let th3 = PROVE_HYP (EXISTS (Choice.get <| mk_exists(v, eq), rs) (REFL rs)) th2
  +    let v_th3 = 
  +        choice {
  +            let! cvs, t = dest_eq tm
  +            let v, vs = strip_comb cvs
  +            let rs = list_mk_abs (vs, t)
  +            let! eq = mk_eq(rs, v)
  +            let th1 =  itlist (fun v th -> CONV_RULE (LAND_CONV BETA_CONV) (AP_THM th v)) (rev vs) (ASSUME eq)
  +            let th2 = SIMPLE_CHOOSE v (SIMPLE_EXISTS v (GENL vs th1))
  +            let! tm = mk_exists(v, eq)
  +            let th3 = PROVE_HYP (EXISTS (tm, rs) (REFL rs)) th2
  +            return (v, th3)
  +        }
       fun (asl, w as gl) -> 
  -            let avoids = itlist (union << frees << concl << Choice.get << snd) asl (frees w)
  -            if mem v avoids
  -            then failwith "ABBREV_TAC: variable already used"
  +        choice {
  +            let! (v, th3) = v_th3 
  +            let! asl' = Choice.List.map snd asl
  +            let avoids = itlist (union << frees << concl) asl' (frees w)
  +            if mem v avoids then 
  +                return! Choice.failwith "ABBREV_TAC: variable already used"
               else 
  -                CHOOSE_THEN (fun th -> 
  +                return! CHOOSE_THEN (fun th -> 
                           RULE_ASSUM_TAC(PURE_ONCE_REWRITE_RULE [th])
                           |> THEN <| PURE_ONCE_REWRITE_TAC [th]
                           |> THEN <| ASSUME_TAC th) th3 gl
  +        }
   
   /// Expand an abbreviation in the hypotheses.
  -let EXPAND_TAC s = FIRST_ASSUM
  -                       (SUBST1_TAC << SYM 
  -                        << Choice.get << check((=) (Choice.result s) << Choice.map fst << Choice.bind dest_var << Choice.bind rhs << Choice.map concl))
  -                   |> THEN <| BETA_TAC
  +let EXPAND_TAC s = 
  +    let f thm =
  +        match check ((=) (Choice.result s) << Choice.map fst << Choice.bind dest_var << Choice.bind rhs << Choice.map concl) thm with
  +        | Success th -> th
  +        | Error ex -> Choice2Of2 ex
  +    FIRST_ASSUM (SUBST1_TAC << SYM << f)
  +    |> THEN <| BETA_TAC
  
positive.code:         Simpset(net'', basic_prover, [], rewmaker)
  
  /// Simplify a term repeatedly by conditional contextual rewriting.
  let SIMP_CONV thl = SIMPLIFY_CONV (basic_ss []) thl
  
  /// Simplify a term repeatedly by conditional contextual rewriting, not using default simplications.
  let PURE_SIMP_CONV thl = SIMPLIFY_CONV empty_ss thl
  
  /// Simplify a term once by conditional contextual rewriting.
  let ONCE_SIMP_CONV thl = ONCE_SIMPLIFY_CONV (basic_ss []) thl
  
  /// Simplify conclusion of a theorem repeatedly by conditional contextual rewriting.
  let SIMP_RULE thl = CONV_RULE(SIMP_CONV thl)
  
  /// Simplify conclusion of a theorem repeatedly by conditional contextual rewriting, not using default simplifications.
  let PURE_SIMP_RULE thl = CONV_RULE(PURE_SIMP_CONV thl)
  
  /// Simplify conclusion of a theorem once by conditional contextual rewriting.
  let ONCE_SIMP_RULE thl = CONV_RULE(ONCE_SIMP_CONV thl)
  
  /// Simplify a goal repeatedly by conditional contextual rewriting.
  let SIMP_TAC thl = CONV_TAC(SIMP_CONV thl)
  
  /// Simplify a goal repeatedly by conditional contextual rewriting without default simplifications.
  let PURE_SIMP_TAC thl = CONV_TAC(PURE_SIMP_CONV thl)
  
  /// Simplify conclusion of goal once by conditional contextual rewriting.
  let ONCE_SIMP_TAC thl = CONV_TAC(ONCE_SIMP_CONV thl)
  
  /// Perform simplification of goal by conditional contextual rewriting using assumptions and
  /// built-in simplifications.
  let ASM_SIMP_TAC = ASM SIMP_TAC
  
  /// Perform simplification of goal by conditional contextual rewriting using assumptions.
  let PURE_ASM_SIMP_TAC = ASM PURE_SIMP_TAC
  
  /// Simplify toplevel applicable terms in goal using assumptions and context.
  let ONCE_ASM_SIMP_TAC = ASM ONCE_SIMP_TAC
  
  (* ------------------------------------------------------------------------- *)
  (* Abbreviation tactics.                                                     *)
  
negative.code: /// General simplification with given strategy and simpset and theorems.
  let GEN_SIMPLIFY_CONV (strat : strategy) ss lev thl = 
      let ss' = itlist AUGMENT_SIMPSET thl ss
      TRY_CONV (strat ss' lev)
  
  /// General top-level simplification with arbitrary simpset.
  let ONCE_SIMPLIFY_CONV ss = 
      GEN_SIMPLIFY_CONV ONCE_DEPTH_SQCONV ss 1
  
  /// General simplification at depth with arbitrary simpset.
  let SIMPLIFY_CONV ss = 
      GEN_SIMPLIFY_CONV TOP_DEPTH_SQCONV ss 3
  
  (* ------------------------------------------------------------------------- *)
  (* Simple but useful default version.                                        *)
  (* ------------------------------------------------------------------------- *)
  
  /// Simpset consisting of only the default rewrites and conversions.
  let empty_ss = 
      Simpset(empty_net, basic_prover, [], fun x y -> Choice.get <| mk_rewrites true x y)
  
  /// Construct a straightforward simpset from a list of theorems.
  let basic_ss = 
  