diff -r 0a869029ca58 -r 6fe9cb1da9ed src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Fri Oct 28 02:23:49 2005 +0200
+++ b/src/HOL/Tools/res_clause.ML	Fri Oct 28 02:24:58 2005 +0200
@@ -60,7 +60,15 @@
   val make_fixed_const : String.string -> string		
   val make_fixed_type_const : String.string -> string   
   val make_type_class : String.string -> string
-
+  val isMeta : String.string -> bool
+  
+  type typ_var
+  val mk_typ_var_sort : Term.typ -> typ_var * sort
+  type type_literal
+  val add_typs_aux2 : (typ_var * string list) list -> type_literal list * type_literal list
+  val gen_tptp_cls : int * string * string * string -> string
+  val gen_tptp_type_cls : int * string * string * string * int -> string
+  val tptp_of_typeLit : type_literal -> string
   end;
 
 structure ResClause: RES_CLAUSE =
@@ -212,6 +220,10 @@
 
 datatype typ_var = FOLTVar of indexname | FOLTFree of string;
 
+fun mk_typ_var_sort (TFree(a,s)) = (FOLTFree a,s)
+  | mk_typ_var_sort (TVar(v,s)) = (FOLTVar v,s);
+
+
 
 (* ML datatype used to repsent one single clause: disjunction of literals. *)
 datatype clause = 
@@ -495,6 +507,21 @@
 	  (vss, fs union fss, preds'')
       end;
 
+fun add_typs_aux2 [] = ([],[])
+  | add_typs_aux2 ((FOLTVar indx,s)::tss) =
+    let val vs = sorts_on_typs (FOLTVar indx,s)
+	val (vss,fss) = add_typs_aux2 tss
+    in
+	(vs union vss,fss)
+    end
+  | add_typs_aux2 ((FOLTFree x,s)::tss) =
+    let val fs = sorts_on_typs (FOLTFree x,s)
+	val (vss,fss) = add_typs_aux2 tss
+    in
+	(vss,fs union fss)
+    end;
+
+
 fun add_typs (Clause cls) preds  = add_typs_aux (#types_sorts cls) preds