anchor.diff:  /// Strips an abstraction from each side of an equational goal.
   let (ABS_TAC : tactic) = 
       fun (asl, w) -> 
  -        let v = 
  -            let l, r = Choice.get <| dest_eq w
  -            let lv, lb = Choice.get <| dest_abs l
  -            let rv, rb = Choice.get <| dest_abs r
  -            let avoids = itlist (union << thm_frees << Choice.get << snd) asl (frees w)
  -            let v = Choice.get <| mk_primed_var avoids lv
  -            (null_meta, [asl, Choice.get <| mk_eq(Choice.get <| vsubst [v, lv] lb, Choice.get <| vsubst [v, rv] rb)], 
  -             fun i tl -> 
  -                let fun1 l =
  -                    match l with
  -                    | [a] -> a
  -                    | _ -> Choice.failwith "ABS_TAC.fun1: Unhandled case."
  -                let ath = ABS v (fun1 tl)
  -                EQ_MP (ALPHA (concl <| Choice.get ath) (Choice.get <| instantiate i w)) ath)
  -            |> Choice.result
  -        v |> Choice.mapError (fun e -> nestedFailure e "ABS_TAC: Failure.")
  +        choice { 
  +            let! l, r = dest_eq w
  +            let! lv, lb = dest_abs l
  +            let! rv, rb = dest_abs r
  +            let! asl' = Choice.List.map snd asl
  +            let avoids = itlist (union << thm_frees) asl' (frees w)
  +            let! v = mk_primed_var avoids lv
  +            let! tm1 = vsubst [v, lv] lb
  +            let! tm2 = vsubst [v, rv] rb
  +            let! tm3 = mk_eq(tm1, tm2)
  +            return 
  +                (null_meta, [asl, tm3], 
  +                 fun i tl -> 
  +                    let fun1 l =
  +                        match l with
  +                        | [a] -> a
  +                        | _ -> Choice.failwith "ABS_TAC.fun1: Unhandled case."
  +                    choice {
  +                        let ath = ABS v (fun1 tl)
  +                        let! tm = Choice.map concl ath
  +                        return! EQ_MP (ALPHA tm (Choice.get <| instantiate i w)) ath
  +                    })            
  +        }
  +        |> Choice.mapError (fun e -> nestedFailure e "ABS_TAC: Failure.")
   
   /// Breaks down a goal between function applications into equality of functions and arguments.
   let (MK_COMB_TAC : tactic) = 
       fun (asl, gl) -> 
  -        let v = 
  +        choice { 
               let fun1 l =
                   match l with
                   | [a1; a2] -> (a1, a2)
                   | _ -> failwith "MK_COMB_TAC.fun1: Unhandled case."
  -            let l, r = Choice.get <| dest_eq gl
  -            let f, x = Choice.get <| dest_comb l
  -            let g, y = Choice.get <| dest_comb r
  -            (null_meta, [asl, Choice.get <| mk_eq(f, g); asl, Choice.get <| mk_eq(x, y)], fun _ tl -> MK_COMB (fun1 tl))
  -            |> Choice.result
  -        v |> Choice.mapError (fun e -> nestedFailure e "MK_COMB_TAC: Failure.")
  +            let! l, r = dest_eq gl
  +            let! f, x = dest_comb l
  +            let! g, y = dest_comb r
  +            let! tm1 = mk_eq(f, g)
  +            let! tm2 = mk_eq(x, y)
  +            return (null_meta, [asl, tm1; asl, tm2], fun _ tl -> MK_COMB (fun1 tl))            
  +        } 
  +        |> Choice.mapError (fun e -> nestedFailure e "MK_COMB_TAC: Failure.")
   
   /// Strips a function application from both sides of an equational goal.
   let (AP_TERM_TAC : tactic) =
  
positive.code:         |> Choice.mapError (fun e -> nestedFailure e "AP_THM_TAC")
  
  /// Makes a simple term substitution in a goal using a single equational theorem.
  let (SUBST1_TAC : thm_tactic) = fun th -> CONV_TAC(SUBS_CONV [th])
  
  /// Substitutes using a single equation in both the assumptions and conclusion of a goal.
  let SUBST_ALL_TAC rth =
      SUBST1_TAC rth |> THEN <| RULE_ASSUM_TAC (SUBS [rth])
  
  /// Beta-reduces all the beta-redexes in the conclusion of a goal.
  let BETA_TAC = CONV_TAC(REDEPTH_CONV BETA_CONV)
  
  (* ------------------------------------------------------------------------- *)
  (* Just use an equation to substitute if possible and uninstantiable.        *)
  
negative.code: 
  /// Use an equation to substitute "safely" in goal.
  let SUBST_VAR_TAC (th : thm) g : goalstate = 
      choice { 
          let! asm, eq = Choice.map dest_thm th
          let! l, r = dest_eq eq
          if aconv l r then 
              return! ALL_TAC g
          elif not(subset (frees eq) (freesl asm)) then 
              return! Choice.failwith ""
          elif (is_const l || is_var l) && not(free_in l r) then 
              return! SUBST_ALL_TAC th g
          elif (is_const r || is_var r) && not(free_in r l) then
              return! SUBST_ALL_TAC (SYM th) g
          else 
              return! Choice.failwith ""
      } 
      |> Choice.mapError (fun e -> nestedFailure e "SUBST_VAR_TAC")
  
  (* ------------------------------------------------------------------------- *)
  (* Basic logical tactics.                                                    *)
  