anchor.diff:      (* ------------------------------------------------------------------------- *)
   
       /// Returns the type of a term.
  -    let type_of tm = 
  -        let rec type_of tm = 
  +    // OPTIMIZE : Use ChoiceCont from ExtCore here to recurse in bounded stack space.
  +    let type_of tm : Choice<hol_type, exn> =
  +        let rec type_of tm =
  +            choice {
               match tm with
  -            | Var(_, ty) -> ty
  -            | Const(_, ty) -> ty
  -            | Comb(s, _) -> hd(tl(snd(Choice.get <| dest_type(type_of s))))
  -            | Abs(Var(_, ty), t) -> 
  -                Tyapp("fun", [ty; type_of t])
  -            | _ -> failwith "type_of: not a type of a term"
  -
  -        Choice.attempt <| fun () ->
  -            type_of tm
  +            | Var(_, ty) ->
  +                return ty
  +            | Const(_, ty) ->
  +                return ty
  +            | Comb(s, _) ->
  +                let! type_of_s = type_of s
  +                let! dest_type_of_s = dest_type type_of_s
  +                return hd (tl (snd dest_type_of_s))
  +            | Abs(Var(_, ty), t) ->
  +                let! type_of_t = type_of t
  +                return Tyapp("fun", [ty; type_of_t])
  +            | _ ->
  +                return! Choice.failwith "type_of: not a type of a term"
  +            }
  +
  +        type_of tm
       
       (* ------------------------------------------------------------------------- *)
       (* Primitive discriminators.                                                 *)
  
positive.code:     (* ------------------------------------------------------------------------- *)
  
      /// Instantiates types in a theorem.
      let INST_TYPE theta (thm : thm) : thm =
          // TODO: revise this
          let INST_TYPE theta (Sequent(asl, c)) : thm =
              Choice.attempt <| fun () ->
                  let inst_fn = Choice.get << inst theta
                  Sequent(term_image inst_fn asl, inst_fn c)
          Choice.bind (INST_TYPE theta) thm
      
      /// Instantiates free variables in a theorem.
  
negative.code:         // TODO: revise this
          let INST theta (Sequent(asl, c)) : thm =
              Choice.attempt <| fun () ->
                  let inst_fun : term -> term = Choice.get << vsubst theta
                  Sequent(term_image inst_fun asl, inst_fun c)
          Choice.bind (INST theta) thm
      
  