Now includes only types used to instantiate overloaded constants in arity clauses

--- a/src/HOL/Tools/res_atp.ML	Thu Nov 16 01:07:39 2006 +0100
+++ b/src/HOL/Tools/res_atp.ML	Thu Nov 16 17:05:23 2006 +0100
@@ -666,10 +666,17 @@
 
 val add_type_consts_in_type = fold_type_consts setinsert;
 
-val add_type_consts_in_term = fold_types add_type_consts_in_type;
+(*Type constructors used to instantiate overloaded constants are the only ones needed.*)
+fun add_type_consts_in_term thy =
+  let val const_typargs = Sign.const_typargs thy
+      fun add_tcs (Const cT) x = fold add_type_consts_in_type (const_typargs cT) x
+        | add_tcs (Abs (_, T, u)) x = add_tcs u x
+        | add_tcs (t $ u) x = add_tcs t (add_tcs u x)
+        | add_tcs _ x = x
+  in  add_tcs  end
 
-fun type_consts_of_terms ts =
-  Symtab.keys (fold add_type_consts_in_term ts Symtab.empty);
+fun type_consts_of_terms thy ts =
+  Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty);
 
 
 (***************************************************************)
@@ -722,7 +729,7 @@
         val subs = tfree_classes_of_terms (map prop_of goal_cls)
         and axtms = map (prop_of o #1) axclauses
         val supers = tvar_classes_of_terms axtms
-        and tycons = type_consts_of_terms axtms
+        and tycons = type_consts_of_terms thy axtms
         (*TFrees in conjecture clauses; TVars in axiom clauses*)
         val classrel_clauses = 
               if keep_types then ResClause.make_classrel_clauses thy subs supers
@@ -854,7 +861,7 @@
                 val subs = tfree_classes_of_terms (map prop_of ccls)
                 and axtms = map (prop_of o #1) axcls
                 val supers = tvar_classes_of_terms axtms
-                and tycons = type_consts_of_terms axtms
+                and tycons = type_consts_of_terms thy axtms
                 (*TFrees in conjecture clauses; TVars in axiom clauses*)
                 val classrel_clauses = 
                       if keep_types then ResClause.make_classrel_clauses thy subs supers