# HG changeset patch
# User paulson
# Date 1176379082 -7200
# Node ID 8a70bc64483351002516b17b26db18c73cf573f2
# Parent  f10465ee7aa21c3ca2efbbd295a52b795a0cfcfe
Improved treatment of classrel/arity clauses

diff -r f10465ee7aa2 -r 8a70bc644833 src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Thu Apr 12 13:57:27 2007 +0200
+++ b/src/HOL/Tools/res_atp.ML	Thu Apr 12 13:58:02 2007 +0200
@@ -739,8 +739,8 @@
         val supers = tvar_classes_of_terms axtms
         and tycons = type_consts_of_terms thy (goal_tms@axtms)
         (*TFrees in conjecture clauses; TVars in axiom clauses*)
-        val classrel_clauses = ResClause.make_classrel_clauses thy subs supers
-        val arity_clauses = ResClause.arity_clause_thy thy tycons supers
+        val (supers',arity_clauses) = ResClause.make_arity_clauses thy tycons supers
+        val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
         val writer = if dfg then dfg_writer else tptp_writer
         and file = atp_input_file()
         and user_lemmas_names = map #1 user_rules
@@ -863,10 +863,10 @@
                 and supers = tvar_classes_of_terms axtms
                 and tycons = type_consts_of_terms thy (ccltms@axtms)
                 (*TFrees in conjecture clauses; TVars in axiom clauses*)
-                val classrel_clauses = ResClause.make_classrel_clauses thy subs supers
+                val (supers',arity_clauses) = ResClause.make_arity_clauses thy tycons supers
+                val _ = Output.debug (fn () => "arity clauses = " ^ Int.toString (length arity_clauses))
+                val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
                 val _ = Output.debug (fn () => "classrel clauses = " ^ Int.toString (length classrel_clauses))
-                val arity_clauses = ResClause.arity_clause_thy thy tycons supers
-                val _ = Output.debug (fn () => "arity clauses = " ^ Int.toString (length arity_clauses))
                 val clnames = writer logic ccls fname (axcls,classrel_clauses,arity_clauses) []
                 val thm_names = Vector.fromList clnames
                 val _ = if !Output.debugging then trace_vector fname thm_names else ()