anchor.diff:      let p = parse_term @"p:bool"
       let q = parse_term @"q:bool"
       let pth =
  -        
  -        SYM(BETA_RULE(AP_THM (AP_THM IMP_DEF p) q))
  -    fun a th -> 
  -        choice {
  -            let th1 = CONJ (ASSUME a) th
  -            let! tm1 = Choice.map concl th1
  -            let th2 = CONJUNCT1(ASSUME tm1)
  -            let th3 = DEDUCT_ANTISYM_RULE th1 th2
  -            let! tm = Choice.map concl th
  -            let th4 = INST [a, p; tm, q] pth
  -            return! EQ_MP th4 th3
  +        choice {
  +        let! IMP_DEF = IMP_DEF
  +        let! foo1 = AP_THM (Choice.result IMP_DEF) p
  +        let! foo2 = AP_THM (Choice.result foo1) q
  +        let! foo3 = BETA_RULE (Choice.result foo2)
  +        return! SYM (Choice.result foo3)
  +        }
  +    fun a (th : Protected<thm0>) -> 
  +        choice {
  +        let! pth = pth
  +        let! th = th
  +        let! foo1 = ASSUME a
  +        let! th1 = CONJ (Choice.result foo1) (Choice.result th)
  +        let tm1 = concl th1
  +        let! foo2 = ASSUME tm1
  +        let! th2 = CONJUNCT1 (Choice.result foo2)
  +        let! th3 = DEDUCT_ANTISYM_RULE (Choice.result th1) (Choice.result th2)
  +        let tm = concl th
  +        let! th4 = INST [a, p; tm, q] (Choice.result pth)
  +        return! EQ_MP (Choice.result th4) (Choice.result th3)
           } : Protected<thm0>
   
   /// Discharges all hypotheses of a theorem.
   let rec DISCH_ALL (th : Protected<thm0>) : Protected<thm0> = 
       choice {
  -        let! th' = th
  -        match hyp th' with
  -        | t :: _ ->
  -            return! DISCH_ALL(DISCH t th) |> Choice.bindError (function Failure _ -> th | e -> Choice.error e) 
  -        | _ -> 
  -            return! th
  +    let! th' = th
  +    match hyp th' with
  +    | t :: _ ->
  +        // TODO : Un-nest this -- but make sure we propagate the error correctly to preserve the original behavior.
  +        return! DISCH_ALL(DISCH t th) |> Choice.bindError (function Failure _ -> th | e -> Choice.error e) 
  +    | _ -> 
  +        return! th
       }
   
   /// Undischarges the antecedent of an implicative theorem.
  
positive.code:     }
  
  /// Adds an assumption to a theorem.
  let ADD_ASSUM tm th : Protected<thm0> =
      choice {
      let! th = th
      let! foo1 = DISCH tm (Choice.result th)
  
negative.code:         let! th = INST [concl th1, p; concl th2, q] (Choice.result pth)
          let! foo1 = PROVE_HYP (Choice.result th1) (Choice.result th)
          return! PROVE_HYP (Choice.result th2) (Choice.result foo1)
          } : Protected<thm0>
  
  /// Extracts left conjunct of theorem.
  let CONJUNCT1 =
  