# HG changeset patch
# User immler@in.tum.de
# Date 1246194088 -7200
# Node ID a50de97f1b08a089f58d2b562799e624573f5c41
# Parent  8a8cf7b4473928cc5a2916f6b0dd4b49cf8de7ce
whitelist for HOL problems with ext:
as a 'helper clause' ext was not passed to metis, but metis does not include ext

diff -r 8a8cf7b44739 -r a50de97f1b08 src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Sun Jun 28 15:01:28 2009 +0200
+++ b/src/HOL/Tools/res_atp.ML	Sun Jun 28 15:01:28 2009 +0200
@@ -296,7 +296,11 @@
 
 (*The rule subsetI is frequently omitted by the relevance filter. This could be theory data
   or identified with ATPset (which however is too big currently)*)
-val whitelist = [subsetI];
+val whitelist_fo = [subsetI];
+(* ext has been a 'helper clause', always given to the atps.
+  As such it was not passed to metis, but metis does not include ext (in contrast
+  to the other helper_clauses *)
+val whitelist_ho = [ResHolClause.ext];
 
 (*** retrieve lemmas from clasimpset and atpset, may filter them ***)
 
@@ -531,8 +535,9 @@
    create additional clauses based on the information from extra_cls *)
 fun prepare_clauses dfg goal_cls chain_ths axcls extra_cls thy =
   let
-    val white_thms =
-      filter check_named (map ResAxioms.pairname (whitelist @ chain_ths))
+    val isFO = isFO thy goal_cls
+    val white_thms = filter check_named (map ResAxioms.pairname
+      (whitelist_fo @ (if isFO then [] else whitelist_ho) @ chain_ths))
     val white_cls = ResAxioms.cnf_rules_pairs thy white_thms
     val extra_cls = white_cls @ extra_cls
     val axcls = white_cls @ axcls
@@ -546,7 +551,7 @@
     (*TFrees in conjecture clauses; TVars in axiom clauses*)
     val conjectures = ResHolClause.make_conjecture_clauses dfg thy ccls
     val (clnames,axiom_clauses) = ListPair.unzip (ResHolClause.make_axiom_clauses dfg thy axcls)
-    val helper_clauses = ResHolClause.get_helper_clauses dfg thy (isFO thy goal_cls) (conjectures, extra_cls, [])
+    val helper_clauses = ResHolClause.get_helper_clauses dfg thy isFO (conjectures, extra_cls, [])
     val (supers',arity_clauses) = ResClause.make_arity_clauses_dfg dfg thy tycons supers
     val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
   in
diff -r 8a8cf7b44739 -r a50de97f1b08 src/HOL/Tools/res_hol_clause.ML
--- a/src/HOL/Tools/res_hol_clause.ML	Sun Jun 28 15:01:28 2009 +0200
+++ b/src/HOL/Tools/res_hol_clause.ML	Sun Jun 28 15:01:28 2009 +0200
@@ -423,7 +423,7 @@
         val S = if needed "c_COMBS"
                 then (Output.debug (fn () => "Include combinator S"); cnf_helper_thms thy [comb_S])
                 else []
-        val other = cnf_helper_thms thy [ext,fequal_imp_equal,equal_imp_fequal]
+        val other = cnf_helper_thms thy [fequal_imp_equal,equal_imp_fequal]
     in
         map #2 (make_axiom_clauses dfg thy (other @ IK @ BC @ S))
     end;