# 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