# HG changeset patch
# User mengj
# Date 1135049266 -3600
# Node ID 4b517881ac7ecb4f9676dac4dc6c4ef347cbf53e
# Parent  b8d86717791650926b7540f1802410bd50920e6a
Added functions for fol_type; also put some functions to the signature, used by ResHolClause.

diff -r b8d867177916 -r 4b517881ac7e src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Mon Dec 19 16:07:19 2005 +0100
+++ b/src/HOL/Tools/res_clause.ML	Tue Dec 20 04:27:46 2005 +0100
@@ -73,6 +73,14 @@
   val clause_eq : clause * clause -> bool
   val hash1_clause : clause -> word
 
+  val list_ord : ('a * 'b -> order) -> 'a list * 'b list -> order
+  type fol_type
+  val types_ord : fol_type list * fol_type list -> order
+  val string_of_fol_type : fol_type -> string
+  val mk_fol_type: string * string * fol_type list -> fol_type
+  val types_eq :fol_type list * fol_type list ->
+   (string * string) list * (string * string) list -> bool * ((string * string) list * (string * string) list)
+  val check_var_pairs: ''a * ''b -> (''a * ''b) list -> int
   end;
 
 structure ResClause : RES_CLAUSE =
@@ -233,6 +241,11 @@
 	tcon ^ (paren_pack tstrs)
     end;
 
+fun mk_fol_type ("Var",x,_) = AtomV(x)
+  | mk_fol_type ("Fixed",x,_) = AtomF(x)
+  | mk_fol_type ("Comp",con,args) = Comp(con,args)
+
+
 
 datatype type_literal = LTVar of string | LTFree of string;
 
@@ -342,6 +355,7 @@
       end;
 
 
+
 fun const_types_of (c,T) = types_of (!const_typargs (c,T));
 
 (* Any variables created via the METAHYPS tactical should be treated as