src/HOL/Tools/res_clause.ML

     | Comp of string * fol_type list
   val string_of_fol_type : fol_type -> string
   datatype type_literal = LTVar of string * string | LTFree of string * string
   val mk_typ_var_sort: typ -> typ_var * sort
   exception CLAUSE of string * term
-  val init : theory -> unit
   val isMeta : string -> bool
   val add_typs_aux : (typ_var * string list) list -> type_literal list * type_literal list
   val get_tvar_strs: (typ_var * sort) list -> string list
   datatype arLit =
       TConsLit of class * string * string list

 
 
 exception CLAUSE of string * term;
 
 
-(*Declarations of the current theory--to allow suppressing types.*)
-val const_typargs = ref (Library.K [] : (string*typ -> typ list));
-
-fun num_typargs(s,T) = length (!const_typargs (s,T));
-
-(*Initialize the type suppression mechanism with the current theory before
-    producing any clauses!*)
-fun init thy = (const_typargs := Sign.const_typargs thy);
-
-
 (*Flatten a type to a fol_type while accumulating sort constraints on the TFrees and
   TVars it contains.*)
 fun type_of (Type (a, Ts)) =
       let val (folTyps, ts) = types_of Ts
           val t = make_fixed_type_const a