anchor.diff:      (* Finds the type of a term (assumes it is well-typed).                      *)
       (* ------------------------------------------------------------------------- *)
   
  +    /// Returns the type of a term.
       let rec type_of tm = 
           match tm with
           | Var(_, ty) -> ty
  
positive.code:     (* Finds the type variables (free) in a term.                                *)
      (* ------------------------------------------------------------------------- *)
  
      let rec type_vars_in_term tm = 
          match tm with
          | Var(_, ty) -> tyvars ty
  
negative.code:     (* Handling of (term) definitions.                                           *)
      (* ------------------------------------------------------------------------- *)
  
      /// List of all definitions introduced so far.
      let the_definitions = ref([] : thm list)
      /// Returns the current set of primitive definitions.
      let definitions() = !the_definitions
      
      /// Makes a simple new definition of the form 'c = t'.
      let new_basic_definition tm = 
          match tm with
          | Comb(Comb(Const("=", _), Var(cname, ty)), r) -> 
  