anchor.diff:  let mk_exists = mk_binder "?"
   
   /// Multiply existentially quantifies both sides of an equation using the given variables.
  -let list_mk_exists(vs, bod) : Protected<term> = 
  +let list_mk_exists(vs, bod) : Protected<term> =
       Choice.List.fold (fun acc x -> mk_exists(x, acc)) bod vs
   
   /// Introduces existential quantification given a particular witness.
  -let EXISTS = 
  +let EXISTS =
       let P = parse_term @"P:A->bool"
       let x = parse_term @"x:A"
       let pth =
  -        let th1 = CONV_RULE (RAND_CONV BETA_CONV) (AP_THM EXISTS_DEF P)
  -        let th2 = SPEC (parse_term @"x:A") (ASSUME <| parse_term @"!x:A. P x ==> Q")
  -        let th3 = DISCH (parse_term @"!x:A. P x ==> Q") (MP th2 (ASSUME <| parse_term @"(P:A->bool) x"))
  -        EQ_MP (SYM th1) (GEN (parse_term @"Q:bool") th3)
  +        choice {
  +        let! EXISTS_DEF = EXISTS_DEF
  +        let! foo1 = AP_THM (Choice.result EXISTS_DEF) P
  +        let! th1 = CONV_RULE (RAND_CONV BETA_CONV) (Choice.result foo1)
  +        let! foo2 = ASSUME <| parse_term @"!x:A. P x ==> Q"
  +        let! th2 = SPEC (parse_term @"x:A") (Choice.result foo2)
  +        let! foo3 = ASSUME <| parse_term @"(P:A->bool) x"
  +        let! foo4 = MP (Choice.result th2) (Choice.result foo3)
  +        let! th3 =
  +            let tm = parse_term @"!x:A. P x ==> Q"
  +            DISCH tm (Choice.result foo4)
  +        let! foo5 = SYM (Choice.result th1)
  +        let! foo6 = GEN (parse_term @"Q:bool") (Choice.result th3)
  +        return! EQ_MP (Choice.result foo5) (Choice.result foo6)
  +        }
   
       fun (etm, stm) (th : Protected<thm0>) -> 
           choice {
           let! pth = pth
  +        let! th = th
           let! qf, abs = dest_comb etm
  -        let bth = Choice.bind BETA_CONV (mk_comb(abs, stm))
  +        let! foo1 = mk_comb(abs, stm)
  +        let! bth = BETA_CONV foo1
           let! sty = type_of stm
  -        let cth : Protected<thm0> = PINST [sty, aty] [abs, P; stm, x] (Choice.result pth)
  -        return! PROVE_HYP (EQ_MP (SYM bth) th) cth
  +        let! cth = PINST [sty, aty] [abs, P; stm, x] (Choice.result pth)
  +        let! foo2 = SYM (Choice.result bth)
  +        let! foo3 = EQ_MP (Choice.result foo2) (Choice.result th)
  +        return! PROVE_HYP (Choice.result foo3) (Choice.result cth)
           }
           |> Choice.mapError (fun e -> nestedFailure e "EXISTS") : Protected<thm0>
   
   /// Introduces an existential quantifier over a variable in a theorem.
  -let SIMPLE_EXISTS v (th : Protected<thm0>) : Protected<thm0> = 
  -    choice {
  -        let! tm = Choice.map concl th
  -        let! tm' = mk_exists(v, tm)
  -        return! EXISTS (tm', v) th
  +let SIMPLE_EXISTS v (th : Protected<thm0>) : Protected<thm0> =
  +    choice {
  +    let! th = th
  +    let tm = concl th
  +    let! tm' = mk_exists(v, tm)
  +    return! EXISTS (tm', v) (Choice.result th)
       }
   
   /// Eliminates existential quantification using deduction from a particular witness.
  -let CHOOSE = 
  +let CHOOSE =
       let P = parse_term @"P:A->bool"
       let Q = parse_term @"Q:bool"
  -    let pth = 
  -        let (th1 : Protected<thm0>) = CONV_RULE (RAND_CONV BETA_CONV) (AP_THM EXISTS_DEF P)
  -        let (th2 : Protected<thm0>) = SPEC (parse_term @"Q:bool") (UNDISCH(fst(EQ_IMP_RULE th1)))
  -        DISCH_ALL(DISCH (parse_term @"(?) (P:A->bool)") (UNDISCH th2))
  -    fun (v, th1 : Protected<thm0>) (th2 : Protected<thm0>) -> 
  -        choice {
  -            let! pth = pth
  -            let! th1 = th1
  -            let! th2 = th2
  -            let! abs = rand <| concl th1
  -            let! bv, bod = dest_abs abs
  -            let! cmb = mk_comb(abs, v)
  -            let! pat = vsubst [v, bv] bod
  -            let th3 = CONV_RULE BETA_CONV (ASSUME cmb)
  -            let th4 = GEN v (DISCH cmb (MP (DISCH pat (Choice.result th2)) th3))
  -            let! (_, ty) = dest_var v
  -            let! tm2 = Choice.map concl (Choice.result th2)
  -            let th5 = 
  -                PINST [ty, aty] [abs, P; tm2, Q] (Choice.result pth)
  -            return! MP (MP th5 th4) (Choice.result th1)
  +    let pth =
  +        choice {
  +        let! EXISTS_DEF = EXISTS_DEF
  +        let! foo1 = AP_THM (Choice.result EXISTS_DEF) P
  +        let! th1 = CONV_RULE (RAND_CONV BETA_CONV) (Choice.result foo1)
  +        let! foo2 = EQ_IMP_RULE' (Choice.result th1)
  +        let! foo3 = UNDISCH(Choice.result <| fst foo2)
  +        let! th2 = SPEC Q (Choice.result foo3)
  +        let! foo4 = UNDISCH (Choice.result th2)
  +        let! foo5 = DISCH (parse_term @"(?) (P:A->bool)") (Choice.result foo4)
  +        return! DISCH_ALL (Choice.result foo5)
  +        }
  +    fun (v, th1 : Protected<thm0>) (th2 : Protected<thm0>) ->
  +        choice {
  +        let! pth = pth
  +        let! th1 = th1
  +        let! th2 = th2
  +        let! abs = rand <| concl th1
  +        let! bv, bod = dest_abs abs
  +        let! cmb = mk_comb(abs, v)
  +        let! pat = vsubst [v, bv] bod
  +        let! foo1 = ASSUME cmb
  +        let! th3 = CONV_RULE BETA_CONV (Choice.result foo1)
  +        let! foo2 = DISCH pat (Choice.result th2)
  +        let! foo3 = MP (Choice.result foo2) (Choice.result th3)
  +        let! foo4 = DISCH cmb (Choice.result foo3)
  +        let! th4 = GEN v (Choice.result foo4)
  +        let! _, ty = dest_var v
  +        let tm2 = concl th2
  +        let! th5 = PINST [ty, aty] [abs, P; tm2, Q] (Choice.result pth)
  +        let! foo5 = MP (Choice.result th5) (Choice.result th4)
  +        return! MP (Choice.result foo5) (Choice.result th1)
           }
           |> Choice.mapError (fun e -> nestedFailure e "CHOOSE") : Protected<thm0>
   
   /// Existentially quantifies a hypothesis of a theorem.
   let SIMPLE_CHOOSE v (th : Protected<thm0>) : Protected<thm0> = 
       choice {
  -        let! th = th
  -        let! ts = Choice.map hyp (Choice.result th)
  -        let! t = mk_exists(v, hd ts)
  -        return! CHOOSE (v, ASSUME t) (Choice.result th)
  +    let! th = th
  +    let ts = hyp th
  +    let! t = mk_exists(v, hd ts)
  +    let! foo1 = ASSUME t
  +    return! CHOOSE (v, Choice.result foo1) (Choice.result th)
       }
   
   (* ------------------------------------------------------------------------- *)
  
positive.code:     let P = parse_term @"P:bool"
      let pth =
          choice {
          // CLEAN : Rename these values to something sensible.
          let! foo1 = AP_THM NOT_DEF P
          let! foo2 = CONV_RULE (RAND_CONV BETA_CONV) (Choice.result foo1)
          return! SYM (Choice.result foo2)
          }
      fun (th : Protected<thm0>) ->
          choice {
          let! foo3 = pth
          let! th = th
          let tm = concl th
          // CLEAN : Rename these values to something sensible.
          let! foo1 = rator tm
          let! foo2 = rand foo1
          let! foo4 = INST [tm, P] (Choice.result foo3)
          return! EQ_MP (Choice.result foo4) (Choice.result th)
          }
          |> Choice.mapError (fun e -> nestedFailure e "NOT_INTRO") : Protected<thm0>
  
negative.code:     if List.isEmpty tms then
          return th
      else
          let! avs =
              let avs =
                  let tm = concl th
                  fst <| chop_list (length tms) (fst <| strip_forall tm)
              Choice.List.map (Choice.map snd << dest_var) avs
          let! tms' = Choice.List.map type_of tms
          let! tyins = Choice.List.fold2 (fun acc x y -> type_match x y acc) [] avs tms'
  
          let! foo1 = INST_TYPE tyins (Choice.result th)
          return! SPECL tms (Choice.result foo1)
  