anchor.diff:      let P = parse_term @"P:bool"
       let pth =
           choice {
  +        let! NOT_DEF = NOT_DEF
           // CLEAN : Rename these values to something sensible.
  -        let! foo1 = AP_THM NOT_DEF P
  +        let! foo1 = AP_THM (Choice.result 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! pth = 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)
  +        let! foo4 = INST [tm, P] (Choice.result pth)
           return! EQ_MP (Choice.result foo4) (Choice.result th)
           }
           |> Choice.mapError (fun e -> nestedFailure e "NOT_INTRO") : Protected<thm0>
  
positive.code:     let P = parse_term @"P:bool"
      let Q = parse_term @"Q:bool"
      let R = parse_term @"R:bool"
      let pth = 
          let (th1 : Protected<thm0>) = CONV_RULE (RAND_CONV BETA_CONV) (AP_THM OR_DEF <| parse_term @"P:bool")
          let (th2 : Protected<thm0>) = CONV_RULE (RAND_CONV BETA_CONV) (AP_THM th1 <| parse_term @"Q:bool")
          let (th3 : Protected<thm0>) = SPEC (parse_term @"R:bool") (EQ_MP th2 (ASSUME <| parse_term @"P \/ Q"))
          UNDISCH(UNDISCH th3)
      fun (th0 : Protected<thm0>) (th1 : Protected<thm0>) (th2 : Protected<thm0>) -> 
          choice {
              let! c1 = Choice.map concl th1
              let! c2 = Choice.map concl th2
              if not(aconv c1 c2) then 
                  return! Choice.failwith "DISJ_CASES"
              else 
                  let! l, r = Choice.bind (dest_disj << concl) th0
                  let th = INST [l, P; r, Q; c1, R] pth
                  return! PROVE_HYP (DISCH r th2) (PROVE_HYP (DISCH l th1) (PROVE_HYP th0 th))                        
          }
          |> Choice.mapError (fun e -> nestedFailure e "DISJ_CASES") : Protected<thm0>
  
  
negative.code:     choice {
      let! th1 = th1
      let! th2 = th2
      // TODO : The next two values should use pattern-matching to return errors when the list
      // is empty; as-is, an exception will be raised and the program will crash.
      let tl1 = hyp th1
      let tl2 = hyp th2
      let! tm = mk_disj(hd tl1, hd tl2)
  