Includes type:sort constraints in its code to collect predicates in axiom clauses.
authorpaulson
Thu Nov 16 17:06:24 2006 +0100 (2006-11-16)
changeset 2139811996e938dfe
parent 21397 2134b81a0b37
child 21399 700ae58d2273
Includes type:sort constraints in its code to collect predicates in axiom clauses.
src/HOL/Tools/res_hol_clause.ML
     1.1 --- a/src/HOL/Tools/res_hol_clause.ML	Thu Nov 16 17:05:23 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Thu Nov 16 17:06:24 2006 +0100
     1.3 @@ -696,15 +696,22 @@
     1.4                         (foldl add_clause_funcs (init_funcs_tab Symtab.empty) clauses)
     1.5                         arity_clauses)
     1.6  
     1.7 -fun preds_of clsrel_clauses arity_clauses = 
     1.8 +fun add_clause_preds (Clause {ctypes_sorts, ...}, preds) =
     1.9 +  foldl ResClause.add_type_sort_preds preds ctypes_sorts
    1.10 +  handle Symtab.DUP a => raise ERROR ("predicate " ^ a ^ " has multiple arities")
    1.11 +
    1.12 +(*Higher-order clauses have only the predicates hBOOL and type classes.*)
    1.13 +fun preds_of_clauses clauses clsrel_clauses arity_clauses = 
    1.14      Symtab.dest
    1.15  	(foldl ResClause.add_classrelClause_preds 
    1.16  	       (foldl ResClause.add_arityClause_preds
    1.17 -		      (Symtab.update ("hBOOL",1) Symtab.empty)
    1.18 +		      (Symtab.update ("hBOOL",1) 
    1.19 +		        (foldl add_clause_preds Symtab.empty clauses))
    1.20  		      arity_clauses)
    1.21  	       clsrel_clauses)
    1.22  
    1.23  
    1.24 +
    1.25  (**********************************************************************)
    1.26  (* write clauses to files                                             *)
    1.27  (**********************************************************************)
    1.28 @@ -781,7 +788,7 @@
    1.29  	val helper_clauses = (#2 o ListPair.unzip o get_helper_clauses) ()
    1.30  	val helper_clauses_strs = (#1 o ListPair.unzip o (map clause2dfg)) helper_clauses
    1.31  	val funcs = funcs_of_clauses (helper_clauses @ conjectures @ axclauses') arity_clauses
    1.32 -	and preds = preds_of classrel_clauses arity_clauses
    1.33 +	and preds = preds_of_clauses axclauses' classrel_clauses arity_clauses
    1.34      in
    1.35  	TextIO.output (out, ResClause.string_of_start probname); 
    1.36  	TextIO.output (out, ResClause.string_of_descrip probname);