anchor.diff:              else Tyapp(tycon, args')
           | _ -> rev_assocd ty i ty
       
  +    /// The type ':bool'.
       let bool_ty = Tyapp("bool", [])
  +    /// The type variable ':A'.
       let aty = Tyvar "A"
       
       (* ------------------------------------------------------------------------- *)
  
positive.code: (* Tests for alpha-convertibility (equality ignoring names in abstractions). *)
  (* ------------------------------------------------------------------------- *)
  
  let aconv s t = alphaorder s t = 0
  (* ------------------------------------------------------------------------- *)
  (* Comparison function on theorems. Currently the same as equality, but      *)
  (* it's useful to separate because in the proof-recording version it isn't.  *)
  (* ------------------------------------------------------------------------- *)
  
  let equals_thm th th' = dest_thm th = dest_thm th'
negative.code:     (* Basic type discriminators.                                                *)
      (* ------------------------------------------------------------------------- *)
  
      /// Tests whether a type is an instance of a type constructor.
      let is_type = can dest_type
      /// Tests a type to see if it is a type variable.
      let is_vartype = can dest_vartype
      
      (* ------------------------------------------------------------------------- *)
      (* Return the type variables in a type and in a list of types.               *)
      (* ------------------------------------------------------------------------- *)
  
      /// Returns a list of the type variables in a type.
      let rec tyvars = function 
          | (Tyapp(_, args)) -> itlist (union << tyvars) args []
          | (Tyvar v as tv) -> [tv]
      
  