anchor.diff:              let tm = concl <| Choice.get th
               try 
                   let l, r = Choice.get <| dest_disj tm
  -                if is_eq l
  -                then 
  +                if is_eq l then 
                       let lth = ASSUME l
                       let lth1 = BRANDE lth
                       let lth2 = BRANDE(SYM lth)
                       let rth = BRAND_TRANS(ASSUME r)
  -                    map (ASSOCIATE << LDISJ_CASES th lth1) rth 
  -                    @ map (ASSOCIATE << LDISJ_CASES th lth2) rth
  +                    map (ASSOCIATE << LDISJ_CASES th lth1) rth @ map (ASSOCIATE << LDISJ_CASES th lth2) rth
                   else 
                       let rth = BRAND_TRANS(ASSUME r)
                       map (LDISJ_CASES th (ASSUME l)) rth
               with
               | Failure _ -> 
  -                if is_eq tm
  -                then 
  -                    [BRANDE th
  +                if is_eq tm then 
  +                    [BRANDE th;
                        BRANDE(SYM th)]
                   else [th]
           let find_eqs = 
  -            Choice.get << 
  -                find_terms(fun t -> 
  -                    try 
  -                        fst(Choice.get <| dest_const t) = "="
  -                    with
  -                    | Failure _ -> false)
  +            Choice.get << find_terms(fun t -> 
  +                              try 
  +                                  fst(Choice.get <| dest_const t) = "="
  +                              with
  +                              | Failure _ -> false)
           let REFLEXATE ths = 
               let eqs = itlist (union << find_eqs << concl << Choice.get) ths []
               let tys = map (hd << snd << Choice.get << dest_type << snd << Choice.get << dest_const) eqs
               let gvs = map genvar tys
               itlist (fun v acc -> (REFL v) :: acc) gvs ths
  -        fun ths ->
  -            /// Tests for failure.
  -            let can f x = 
  -                try f x |> ignore; true
  -                with Failure _ -> false
  -            if exists (can(Choice.get << find_term is_eq << concl << Choice.get)) ths
  -            then 
  +        fun ths -> 
  +            if exists (function Success th -> (Choice.isResult << find_term is_eq << concl) th
  +                              | Error _ -> false) ths then 
                   let ths' = map BRAND_CONGS ths
                   let ths'' = itlist (union' equals_thm << BRAND_TRANS) ths' []
                   REFLEXATE ths''
               else ths
  +
       (* ----------------------------------------------------------------------- *)
       (* Push duplicated copies of poly theorems to match existing assumptions.  *)
       (* ----------------------------------------------------------------------- *)
  -    let POLY_ASSUME_TAC = 
  +
  +    let (POLY_ASSUME_TAC : thm list -> tactic) = 
           let rec uniq' eq = 
               fun l -> 
  -                match l with
  -                | x :: (y :: _ as t) -> 
  -                    let t' = uniq' eq t
  -                    if eq x y
  -                    then t'
  -                    elif t' == t
  -                    then l
  -                    else x :: t'
  -                | _ -> l
  +            match l with
  +            | x :: (y :: _ as t) -> 
  +                let t' = uniq' eq t
  +                if eq x y then t'
  +                elif t' == t then l
  +                else x :: t'
  +            | _ -> l
  +
           let setify' le eq s = uniq' eq (sort le s)
  +
           let rec grab_constants tm acc = 
  -            if is_forall tm || is_exists tm
  -            then grab_constants (Choice.get <| body(Choice.get <| rand tm)) acc
  -            elif is_iff tm || is_imp tm || is_conj tm || is_disj tm
  -            then grab_constants (Choice.get <| rand tm) (grab_constants (Choice.get <| lhand tm) acc)
  -            elif is_neg tm
  -            then grab_constants (Choice.get <| rand tm) acc
  +            if is_forall tm || is_exists tm then grab_constants (Choice.get <| body(Choice.get <| rand tm)) acc
  +            elif is_iff tm || is_imp tm || is_conj tm || is_disj tm then 
  +                grab_constants (Choice.get <| rand tm) (grab_constants (Choice.get <| lhand tm) acc)
  +            elif is_neg tm then grab_constants (Choice.get <| rand tm) acc
               else union (Choice.get <| find_terms is_const tm) acc
  +
           let match_consts(tm1, tm2) = 
               let s1, ty1 = Choice.get <| dest_const tm1
               let s2, ty2 = Choice.get <| dest_const tm2
  -            if s1 = s2
  -            then Choice.get <| type_match ty1 ty2 []
  +            if s1 = s2 then Choice.get <| type_match ty1 ty2 []
               else failwith "match_consts"
  +
           let polymorph mconsts th = 
               let tvs = 
                   subtract (Choice.get <| type_vars_in_term(concl <| Choice.get th)) 
                       (unions(map (Choice.get << type_vars_in_term) (hyp <| Choice.get th)))
  -            if tvs = []
  -            then [th]
  +            if tvs = [] then [th]
               else 
                   let pconsts = grab_constants (concl <| Choice.get th) []
  -                let tyins = 
  -                    mapfilter (Some << match_consts)
  -                        (allpairs (fun x y -> x, y) pconsts mconsts)
  +                let tyins = mapfilter (Some << match_consts) (allpairs (fun x y -> x, y) pconsts mconsts)
                   let ths' = 
  -                    setify' (fun th th' -> dest_thm (Choice.get th) <= dest_thm (Choice.get th')) 
  -                        equals_thm (mapfilter (Some << C INST_TYPE th) tyins)
  -                if ths' = []
  -                then 
  +                    setify' (fun th th' -> dest_thm(Choice.get th) <= dest_thm(Choice.get th')) equals_thm 
  +                        (mapfilter (Some << C INST_TYPE th) tyins)
  +                if ths' = [] then 
                       (warn true "No useful-looking instantiations of lemma"
                        [th])
                   else ths'
  +
           let rec polymorph_all mconsts ths acc = 
  -            if ths = []
  -            then acc
  +            if ths = [] then acc
               else 
                   let ths' = polymorph mconsts (hd ths)
                   let mconsts' = itlist grab_constants (map (concl << Choice.get) ths') mconsts
                   polymorph_all mconsts' (tl ths) (union' equals_thm ths' acc)
  -        fun ths (asl, w as gl) ->
  -                let mconsts = itlist (grab_constants << concl << Choice.get << snd) asl []
  -                let ths' = polymorph_all mconsts ths []
  -                MAP_EVERY ASSUME_TAC ths' gl
  +
  +        fun ths (asl, w as gl) -> 
  +            let mconsts = itlist (grab_constants << concl << Choice.get << snd) asl []
  +            let ths' = polymorph_all mconsts ths []
  +            MAP_EVERY ASSUME_TAC ths' gl
  +
       (* ----------------------------------------------------------------------- *)
       (* Basic HOL MESON procedure.                                              *)
       (* ----------------------------------------------------------------------- *)
  +
       let SIMPLE_MESON_REFUTE min max inc ths = 
           clear_contrapos_cache()
           inferences := 0
           let old_dcutin = !meson_dcutin
  -        if !meson_depth
  -        then meson_dcutin := 100001
  +        if !meson_depth then meson_dcutin := 100001
           else ()
           let ths' = 
  -            if !meson_brand
  -            then perform_brand_modification ths
  +            if !meson_brand then perform_brand_modification ths
               else ths @ create_equality_axioms(map (concl << Choice.get) ths)
           let rules = optimize_rules(fol_of_hol_clauses ths')
  -        let proof, (insts, _, _) = 
  -            solve_goal rules (!meson_depth) min max inc (1, [])
  +        let proof, (insts, _, _) = solve_goal rules (!meson_depth) min max inc (1, [])
           meson_dcutin := old_dcutin
           meson_to_hol insts proof
  +
       let CONJUNCTS_THEN' ttac cth = ttac(CONJUNCT1 cth)
                                      |> THEN <| ttac(CONJUNCT2 cth)
  +
       let PURE_MESON_TAC min max inc gl = 
           reset_vars()
           reset_consts()
           (FIRST_ASSUM CONTR_TAC
  -         |> ORELSE 
  -         <| W(ACCEPT_TAC << SIMPLE_MESON_REFUTE min max inc << map snd << fst)) 
  -            gl
  +         |> ORELSE <| W(ACCEPT_TAC << SIMPLE_MESON_REFUTE min max inc << map snd << fst)) 
  +                        gl
  +
       let QUANT_BOOL_CONV = 
           PURE_REWRITE_CONV 
               [FORALL_BOOL_THM; EXISTS_BOOL_THM; COND_CLAUSES; NOT_CLAUSES; 
                IMP_CLAUSES; AND_CLAUSES; OR_CLAUSES; EQ_CLAUSES; FORALL_SIMP; 
                EXISTS_SIMP]
  +
       let rec SPLIT_TAC n g = 
           ((FIRST_X_ASSUM(CONJUNCTS_THEN' ASSUME_TAC)
             |> THEN <| SPLIT_TAC n)
  
positive.code:                 let gv = genvar(Choice.get <| type_of hv')
                  gstore := (gv, v) :: (!gstore)
                  gv
          reset_vars, fol_of_var, hol_of_bumped_var
      let reset_consts, fol_of_const, hol_of_const = 
          let false_tm = (parse_term @"F")
          let cstore = ref([] : (term * int) list)
          let ccounter = ref 2
          let reset_consts() = 
              cstore := [false_tm, 1]
              ccounter := 2
          let fol_of_const c = 
              let currentconsts = !cstore
              match assoc c currentconsts with
  
negative.code:                     |> THEN <| ASM_MESON_TAC ths
  
  (* ------------------------------------------------------------------------- *)
  (* Also introduce a rule.                                                    *)
  (* ------------------------------------------------------------------------- *)
  
  /// Attempt to prove a term by first-order proof search.
  let MESON ths tm = prove(tm, MESON_TAC ths)
  