anchor.diff:      
       /// Equality version of the Modus Ponens rule.
       let EQ_MP (thm1 : thm) (thm2 : thm) : thm =
  -        let EQ_MP (Sequent(asl1, eq)) (Sequent(asl2, c)) = 
  +        let EQ_MP (Sequent(asl1, eq)) (Sequent(asl2, c)) =
  +            choice {
               match eq with
               | Comb(Comb(Const("=", _), l), r) when alphaorder l c = 0 -> 
  -                Choice.result <| Sequent(term_union asl1 asl2, r)
  -            | _ -> Choice.failwith "EQ_MP"
  +                return Sequent(term_union asl1 asl2, r)
  +            | _ ->
  +                return! Choice.failwith "EQ_MP"
  +            }
           Choice.bind2 EQ_MP thm1 thm2
       
       /// Deduces logical equivalence from deduction in both directions.
  
positive.code:     (* Substitution primitive (substitution for variables only!)                 *)
      (* ------------------------------------------------------------------------- *)
  
      /// Substitute terms for variables inside a term.
      let vsubst = 
          let vsubst ilist tm = 
              let rec vsubst ilist tm = 
                  match tm with
                  | Var(_, _) -> rev_assocd tm ilist tm
                  | Const(_, _) -> tm
                  | Comb(s, t) -> 
                      let s' = vsubst ilist s
                      let t' = vsubst ilist t
                      if s' == s && t' == t then tm
                      else Comb(s', t')
                  | Abs(v, s) -> 
                      let ilist' = filter (fun (t, x) -> x <> v) ilist
                      if ilist' = [] then tm
                      else 
                          let s' = vsubst ilist' s
                          if s' == s then tm
                          elif exists (fun (t, x) -> vfree_in v t && vfree_in x s) ilist' then 
                              let v' = Choice.get <| variant [s'] v
                              Abs(v', vsubst ((v', v) :: ilist') s)
                          else Abs(v, s')
  
              Choice.attempt <| fun () ->
                  vsubst ilist tm
  
          fun theta ->
              if theta = [] then Choice.result
              elif forall (fun (t, x) -> 
                      match type_of t, dest_var x with
                      | Success r1, Success r2 -> r1 = snd r2
                      | _ -> false) theta then vsubst theta
              else fun tm -> Choice.failwith "vsubst: Bad substitution list"
      
      (* ------------------------------------------------------------------------- *)
      (* Type instantiation primitive.                                             *)
      (* ------------------------------------------------------------------------- *)
  
      exception Clash of term
      
      /// Instantiate type variables in a term.
      let inst = 
          let inst env tyin tm =
              let rec inst env tyin tm = 
                  match tm with
                  | Var(n, ty) -> 
                      let ty' = type_subst tyin ty
                      let tm' = 
                          if ty' == ty then tm
                          else Var(n, ty')
                      if compare (rev_assocd tm' env tm) tm = 0 then tm'
                      else raise(Clash tm')
                  | Const(c, ty) -> 
                      let ty' = type_subst tyin ty
                      if ty' == ty then tm
                      else Const(c, ty')
                  | Comb(f, x) -> 
                      let f' = inst env tyin f
                      let x' = inst env tyin x
                      if f' == f && x' == x then tm
                      else Comb(f', x')
                  | Abs(y, t) -> 
                      let y' = inst [] tyin y
                      let env' = (y, y') :: env
                      try 
                          let t' = inst env' tyin t
                          if y' == y && t' == t then tm
                          else Abs(y', t')
                      with
                      | Clash(w') as ex -> 
                          if w' <> y' then raise ex
                          else 
                              let ifrees = map (inst [] tyin) (frees t)
                              let y'' = Choice.get <| variant ifrees y'
                              let z = Var(fst(Choice.get <| dest_var y''), snd(Choice.get <| dest_var y))
                              inst env tyin (Abs(z, Choice.get <| vsubst [z, y] t))
              try
                  Choice.result <| inst env tyin tm
              with 
              | :? Clash as ex ->
                  Choice2Of2 (ex :> exn)
              | Failure s ->
                  Choice.failwith s
  
          fun tyin -> 
              if tyin = [] then Choice.result
              else inst [] tyin
      
      (* ------------------------------------------------------------------------- *)
      (* A few bits of general derived syntax.                                     *)
  
negative.code:     /// Declares a new type or type constructor.
      let new_type(name, arity) =
          if Choice.isResult <| get_type_arity name then 
              Choice.failwith ("new_type: type " + name + " has already been declared")
          else
              the_type_constants := (name, arity) :: (!the_type_constants)
              Choice.result ()
      
      (* ------------------------------------------------------------------------- *)
      (* Basic type constructors.                                                  *)
  