anchor.diff:  
   /// Applies the given theorem-tactic using the result of stripping off one outer
   /// connective from the given theorem.
  -let STRIP_THM_THEN = FIRST_TCL [CONJUNCTS_THEN; DISJ_CASES_THEN; CHOOSE_THEN]
  +let STRIP_THM_THEN = 
  +    FIRST_TCL [CONJUNCTS_THEN; DISJ_CASES_THEN; CHOOSE_THEN]
   
   /// Resolves implicative assumptions with an antecedent.
   let (ANTE_RES_THEN : thm_tactical) = 
       fun ttac ante -> 
  -        ASSUM_LIST(fun asl -> 
  -                let tacs = mapfilter (fun imp -> Some <| ttac(MATCH_MP imp ante)) asl
  -                match tacs with
  -                | [] -> failwith "IMP_RES_THEN"
  -                | _ -> EVERY tacs)
  +        ASSUM_LIST (fun asl -> 
  +            // NOTE: this mapfilter call can throw exception in the original version, but can't return Choice2Of2 case here
  +            // We need to review this to ensure equivalent semantics
  +            let tacs = mapfilter (fun imp -> Some <| ttac(MATCH_MP imp ante)) asl
  +            match tacs with
  +            | [] -> fun tm -> Choice.failwith "IMP_RES_THEN"
  +            | _ -> EVERY tacs)
   
   /// Resolves an implication with the assumptions of a goal.
   let (IMP_RES_THEN : thm_tactical) = 
       fun ttac imp -> 
           ASSUM_LIST(fun asl -> 
  -                let tacs = mapfilter (fun ante -> Some <| ttac(MATCH_MP imp ante)) asl
  -                match tacs with
  -                | [] -> failwith "IMP_RES_THEN"
  -                | _ -> EVERY tacs)
  +            let tacs = mapfilter (fun ante -> Some <| ttac(MATCH_MP imp ante)) asl
  +            match tacs with
  +            | [] -> fun tm -> Choice.failwith "IMP_RES_THEN"
  +            | _ -> EVERY tacs)
   
   /// Splits a theorem into a list of theorems and then adds them to the assumptions.
   let STRIP_ASSUME_TAC = 
       let DISCARD_TAC th = 
  -        let tm = concl <| Choice.get th
  +        let tm = Choice.map concl th
           fun (asl, w as g) -> 
  -                if exists (fun a -> aconv tm (concl <| Choice.get(snd a))) asl
  -                then ALL_TAC g
  -                else Choice.failwith "DISCARD_TAC: not already present"
  +            choice {
  +                let! tm = tm
  +                let! asl' = Choice.List.map snd asl
  +                if exists (fun a -> aconv tm (concl a)) asl' then 
  +                    return! ALL_TAC g
  +                else 
  +                    return! Choice.failwith "DISCARD_TAC: not already present"
  +            }
       
       (REPEAT_TCL STRIP_THM_THEN)(fun gth -> 
  -        FIRST [CONTR_TAC gth
  -               ACCEPT_TAC gth
  -               DISCARD_TAC gth
  +        FIRST [CONTR_TAC gth;
  +               ACCEPT_TAC gth;
  +               DISCARD_TAC gth;
                  ASSUME_TAC gth])
   
   /// Performs structural case analysis, applying theorem-tactic to results.
  -let STRUCT_CASES_THEN ttac = REPEAT_TCL STRIP_THM_THEN ttac
  +let STRUCT_CASES_THEN ttac = 
  +    REPEAT_TCL STRIP_THM_THEN ttac
   
   /// Performs very general structural case analysis.
   let STRUCT_CASES_TAC = 
  -    STRUCT_CASES_THEN (fun th -> SUBST1_TAC th |> ORELSE <| ASSUME_TAC th);;
  +    STRUCT_CASES_THEN (fun th -> SUBST1_TAC th |> ORELSE <| ASSUME_TAC th)
   
   /// Splits a goal by eliminating one outermost connective, applying the given theorem-tactic
   /// to the antecedents of implications.
   let STRIP_GOAL_THEN ttac = 
  -    FIRST [GEN_TAC
  -           CONJ_TAC
  +    FIRST [GEN_TAC;
  +           CONJ_TAC;
              DISCH_THEN ttac]
   
   /// Splits a goal by eliminating one outermost connective.
   let (STRIP_TAC : tactic) = 
       fun g -> 
  -        try 
  -            STRIP_GOAL_THEN STRIP_ASSUME_TAC g
  -        with
  -        | Failure _ -> Choice.failwith "STRIP_TAC"
  +        STRIP_GOAL_THEN STRIP_ASSUME_TAC g
  +        |> Choice.mapError (fun e -> nestedFailure e "STRIP_TAC")
   
   /// Undischarges an assumption and applies theorem-tactic to it.
   let (UNDISCH_THEN : term -> thm_tactic -> tactic) = 
       fun tm ttac (asl, w) -> 
  -        let thp, asl' = Option.get <| remove (fun (_, th) -> aconv (concl <| Choice.get th) tm) asl
  -        ttac (snd thp) (asl', w)
  +        choice {            
  +            let! thp, asl' = 
  +                remove (fun (_, th) -> 
  +                    match th with
  +                    | Success th -> aconv (concl th) tm
  +                    | Error _ -> false) asl
  +                |> Option.toChoiceWithError "remove"
  +
  +            return! ttac (snd thp) (asl', w)
  +        }
   
   /// Applies theorem-tactic to first assumption possible, extracting assumption.
  -let FIRST_X_ASSUM ttac = FIRST_ASSUM(fun th -> UNDISCH_THEN (concl <| Choice.get th) ttac)
  +let FIRST_X_ASSUM ttac = 
  +    FIRST_ASSUM(fun th g -> 
  +        choice {
  +            let! tm = Choice.map concl th
  +            return! UNDISCH_THEN tm ttac g
  +        })
   
   (* ------------------------------------------------------------------------- *)
   (* Subgoaling and freezing variables (latter is especially useful now).      *)
  
positive.code: 
  /// Adds the body of an existentially quantified theorem to the assumptions of a goal.
  let (CHOOSE_TAC : thm_tactic) = 
      fun xth g -> 
          let f = 
              let x = fst(Choice.get <| dest_exists(concl <| Choice.get xth))
              fun (asl, w) -> 
                  let avoids = 
                      itlist (union << thm_frees << Choice.get << snd) asl 
                          (union (frees w) (thm_frees <| Choice.get xth))
                  let x' = Choice.get <| mk_primed_var avoids x
                  X_CHOOSE_TAC x' xth (asl, w)
          f g |> Choice.mapError (fun e -> nestedFailure e "CHOOSE_TAC")
  
  /// Reduces a conjunctive goal to two separate subgoals.
  let (CONJ_TAC : tactic) = 
  
negative.code:         SUBGOAL_THEN tm (LABEL_TAC s) |> THENL <| [p; ALL_TAC]
      |  [] -> fun _ -> Choice.failwith "SUBGOAL_TAC: no subproof given"
  
  /// 'Freezes' a theorem to prevent instantiation of its free variables.
  let (FREEZE_THEN : thm_tactical) = 
      fun ttac th (asl, w) -> 
          choice {
              let! tm = Choice.map concl th
              let! (meta, gl, just) = ttac (ASSUME tm) (asl, w)
              return(meta, gl, fun i l -> PROVE_HYP th (just i l))            
          }
  
  (* ------------------------------------------------------------------------- *)
  (* Metavariable tactics.                                                     *)
  