# HG changeset patch
# User paulson
# Date 1256125708 -3600
# Node ID 33aee615096990df7aa2a48c272d9e4dee757134
# Parent  2b3694001c48ffd31cb7c724b267cb44d76387b1
Removed the hard-wired white list of theorems for sledgehammer

diff -r 2b3694001c48 -r 33aee6150969 src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Wed Oct 21 11:19:11 2009 +0100
+++ b/src/HOL/Tools/res_atp.ML	Wed Oct 21 12:48:28 2009 +0100
@@ -290,15 +290,6 @@
 (* Retrieving and filtering lemmas                             *)
 (***************************************************************)
 
-(*** white list and black list of lemmas ***)
-
-(*The rule subsetI is frequently omitted by the relevance filter.*)
-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 and filter them ***)
 
 (*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute*)
@@ -519,11 +510,8 @@
     val included_cls = included_thms |> ResAxioms.cnf_rules_pairs thy |> make_unique
                                      |> restrict_to_logic thy isFO
                                      |> remove_unwanted_clauses
-    val axcls = relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls)
-    (* add whitelist *)
-    val white_cls = ths_to_cls thy (whitelist_fo @ (if isFO then [] else whitelist_ho))
   in
-    white_cls @ axcls 
+    relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls) 
   end;
 
 (* prepare for passing to writer,