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:             pp_print_break fmt 0 0
              pp_print_list_trmtrmInner fmt tl
          | [] -> ()
      if al.Length = 0
      then pp_print_string fmt "No items"
      else
          pp_open_hvbox fmt 0
          pp_print_list_trmtrmInner fmt al
          pp_close_box fmt ()
  
negative.code:             |> Choice.mapError (fun e -> nestedFailure e "new_definition: Non-variable in LHS pattern")
  
          let! def = mk_eq(lv, rtm)
          let! th1 = new_basic_definition def
          let! th2 = 
              Choice.List.foldBack (fun tm acc -> 
                  choice {
                      let! ith = AP_THM acc tm
                      let! tm1 = rand <| concl ith
                      let! th2 = BETA_CONV tm1
                      return TRANS (Choice.result ith) (Choice.result th2)
                  }) largs (Choice.result th1)
  
          let rvs = filter (not << C mem avs) largs
          return! itlist GEN rvs (itlist GEN avs th2)
  