anchor.diff:                  let! (sth, bod, pbod, lconsts) = v
                   let bvms = match_bvs tm pbod []
                   let! abod = deep_alpha bvms bod
  -                let ath = EQ_MP (ALPHA bod abod) sth
  +                let! ath = EQ_MP (ALPHA bod abod) sth
                   let! tm1 = partfn abod
                   let! insts = term_match lconsts tm1 tm
  -                let fth = INSTANTIATE insts ath
  -                let! fth' = fth
  -                let! ath' = ath
  -                if hyp fth' <> hyp ath' then 
  +                let! fth = INSTANTIATE insts (Choice.result ath)
  +                if hyp fth <> hyp ath then 
                       return! Choice.failwith "PART_MATCH: instantiated hyps"
                   else 
  -                    let! tm' = Choice.bind (partfn << concl) fth
  +                    let! tm' = partfn <| concl fth
                       if compare tm' tm = 0 then 
  -                        return! fth
  +                        return fth
                       else 
                           return!
  -                            SUBS [ALPHA tm' tm] fth
  +                            SUBS [ALPHA tm' tm] (Choice.result fth)
                               |> Choice.mapError (fun e -> nestedFailure e "PART_MATCH: Sanity check failure")
               }
   
       let GEN_PART_MATCH partfn (th : Protected<thm0>) = 
           let v =
               choice {
  -            let sth = SPEC_ALL th
  -            let! bod = Choice.map concl sth
  +            let! sth = SPEC_ALL th
  +            let bod = concl sth
               let! pbod = partfn bod
               let! tm0 = Choice.map concl th
               let! tl = Choice.map hyp th
  
positive.code:             choice {
                  let! bv, bod = dest_abs tm
                  let! tm' = body pat
                  return! ABS bv (HO_BETAS bcs tm' bod)
              }
              |> Choice.bindError (function
                  | Failure _ ->
                      let hop, args = strip_comb pat
                      rev_assoc hop bcs
                      |> Option.toChoiceWithError "find"
                      |> Choice.bind (fun n ->
                          if length args = n then
                              BETAS_CONV n tm
                          else
                              Choice.fail ())
                      |> Choice.bindError (function
                          | Failure _ ->
                              choice {
                                  let! lpat, rpat = dest_comb pat
                                  let! ltm, rtm = dest_comb tm
                          
                                  let! lth = HO_BETAS bcs lpat ltm
                                  let! rth = HO_BETAS bcs rpat rtm
                                  return!
                                      let lth = Choice.result lth in
                                      let rth = Choice.result rth in
                                      MK_COMB(lth, rth)
                                      |> Choice.bindError (fun _ ->
                                          AP_THM lth rtm)
                                      |> Choice.bindError (fun _ ->
                                          choice {
                                          let! rth = HO_BETAS bcs rpat rtm
                                          return! AP_TERM ltm (Choice.result rth)
                                          })
                              }
                           | e -> Choice.error e)
                   | e -> Choice.error e)
  
      fun (bcs, tmin, tyin) th ->
  
negative.code: 
          let rec free_beta v tm = 
              if is_abs tm then 
                  // Choice.get is safe to use here
                  let bv, bod = Choice.get <| dest_abs tm
                  if v = bv then
                      fun _ -> Choice.failwith "unchanged"
                  else
                      ABS_CONV(free_beta v bod)
              else
                  let op, args = strip_comb tm
                  if args = [] then
                      fun _ -> Choice.failwith "unchanged"
                  elif op = v then
                      BETA_CONVS(length args)
                  else
                      let lr = dest_comb tm
                      // NOTE: review this
                      // The original version raises an exception in initialization
                      // We have to evaluate the function with some input in order to determine errors
                      fun tm ->
                          choice {
                          let! (l, r) = lr
                          return!
                              choice { 
                                  let lconv = free_beta v l
                                  // Evaluate with tm to spot errors
                                  let! _ = lconv tm
                                  return!
                                      choice { 
                                          let rconv = free_beta v r
                                          // Evaluate with tm to spot errors
                                          let! _ = rconv tm
                                          return! COMB2_CONV lconv rconv tm
                                      }
                                      |> Choice.bindError (function
                                          | Failure _ ->
                                              RATOR_CONV lconv tm
                                          | e -> Choice.error e)
                              }
                              |> Choice.bindError (function
                                  | Failure _ ->
                                      choice {
                                          let conv = free_beta v r
                                          // Evaluate with tm to spot errors
                                          let! _ = conv tm
                                          return! RAND_CONV conv tm
                                      }
                                  | e -> Choice.error e)
                          }
          free_beta
  
      let GINST (th : Protected<thm0>) =
          choice {
              let! th = th
              let fvs = subtract (frees <| concl th) (freesl <| hyp th)
              let! gvs = Choice.List.map (Choice.map genvar << type_of) fvs
              return! INST (zip gvs fvs) (Choice.result th)
          }
  
      let higher_rewrite_conv ths =
          let v = 
              choice {
                  let! thl = Choice.List.map (GINST << SPEC_ALL) ths
                  let concs = map concl thl
                  let! lefts = Choice.List.map lhs concs
                  let! lefts' = Choice.List.map dest_comb lefts
                  let preds, pats = unzip lefts'
                  let beta_fns = map2 BETA_VAR preds concs
                  let ass_list = zip pats (zip preds (zip thl beta_fns))
                  let! mnet = Choice.List.foldBack (fun p n -> enter [] (p, p) n) pats empty_net
                  return (thl, ass_list, mnet)
              }
  
          let look_fn t =
              choice {
                  // CLEAN : Rename this value to something reasonable.
                  let! (thl, ass_list, mnet) = v
                  let! foo1 = lookup t mnet
                  return
                      foo1
                      |> mapfilter (fun p ->
                          if Choice.isResult <| term_match [] p t then
                              Some p
                          else None) 
              }
  
          fun top tm -> 
              choice {
                  // NOTE: suppress errors in look_fn
                  let pred t = not(look_fn t = Choice.result []) && free_in t tm
  
                  let! (thl, ass_list, mnet) = v
  
                  let! stm = 
                      choice {
                      if top then
                          return! find_term pred tm
                      else
                          let! tms = find_terms pred tm
                          return hd(sort free_in tms)
                      }
                  let! stm' = look_fn stm
                  let pat = hd stm'
                  let! _, tmin, tyin = term_match [] pat stm
                  let! pred, (th, beta_fn) =
                      assoc pat ass_list
                      |> Option.toChoiceWithError "find"
                  let! ty1 = type_of stm
                  let gv = genvar ty1
                  let! tm1 = subst [gv, stm] tm
                  let! abs = mk_abs(gv, tm1)
                  let! _, tmin0, tyin0 = term_match [] pred abs
                  let! th1 = INST_TYPE tyin0 (Choice.result th)
                  let! th2 = INST tmin0 (Choice.result th1)
                  let! th3 = INST tmin (Choice.result th2)
                  return! CONV_RULE beta_fn (Choice.result th3)
              }
  
      fun ths top tm ->
          higher_rewrite_conv ths top tm : Protected<thm0>
  
  (* ------------------------------------------------------------------------- *)
  (* Derived principle of definition justifying |- c x1 .. xn = t[x1,..,xn]    *)
  