# HG changeset patch
# User Philipp Meyer
# Date 1252592178 -7200
# Node ID 4d4ee06e9420713aa84a7e5c9d5c2f5255c480af
# Parent  421323205efd0a22e397447092edff9660b3c386
atp_minimize is now not using whitelist

diff -r 421323205efd -r 4d4ee06e9420 src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Thu Sep 10 15:57:55 2009 +0200
+++ b/src/HOL/Tools/res_atp.ML	Thu Sep 10 16:16:18 2009 +0200
@@ -520,12 +520,17 @@
 fun get_relevant max_new theory_const (ctxt, (chain_ths, th)) goal_cls =
   let
     val thy = ProofContext.theory_of ctxt
+    val isFO = isFO thy goal_cls
     val included_thms = get_clasimp_atp_lemmas ctxt
     val included_cls = included_thms |> ResAxioms.cnf_rules_pairs thy |> make_unique
-                                     |> restrict_to_logic thy (isFO thy goal_cls)
+                                     |> restrict_to_logic thy isFO
                                      |> remove_unwanted_clauses
+    val axcls = relevance_filter max_new theory_const thy included_cls (map prop_of 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
   in
-    relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls)
+    white_cls @ axcls 
   end;
 
 (* prepare for passing to writer,
@@ -533,11 +538,6 @@
 fun prepare_clauses dfg goal_cls chain_ths axcls extra_cls thy =
   let
     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
     val ccls = subtract_cls goal_cls extra_cls
     val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm_global thy th)) ccls
     val ccltms = map prop_of ccls