diff -r 10e723e54076 -r c5f54c04a1aa src/HOL/Tools/res_blacklist.ML
--- a/src/HOL/Tools/res_blacklist.ML	Wed Mar 17 19:55:07 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,43 +0,0 @@
-(*  Title:      HOL/Tools/res_blacklist.ML
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Author:     Makarius
-
-Theorems blacklisted to sledgehammer.  These theorems typically
-produce clauses that are prolific (match too many equality or
-membership literals) and relate to seldom-used facts.  Some duplicate
-other rules.
-*)
-
-signature RES_BLACKLIST =
-sig
-  val setup: theory -> theory
-  val blacklisted: Proof.context -> thm -> bool
-  val add: attribute
-  val del: attribute
-end;
-
-structure Res_Blacklist: RES_BLACKLIST =
-struct
-
-structure Data = Generic_Data
-(
-  type T = thm Termtab.table;
-  val empty = Termtab.empty;
-  val extend = I;
-  fun merge tabs = Termtab.merge (K true) tabs;
-);
-
-fun blacklisted ctxt th =
-  Termtab.defined (Data.get (Context.Proof ctxt)) (Thm.full_prop_of th);
-
-fun add_thm th = Data.map (Termtab.update (Thm.full_prop_of th, th));
-fun del_thm th = Data.map (Termtab.delete_safe (Thm.full_prop_of th));
-
-val add = Thm.declaration_attribute add_thm;
-val del = Thm.declaration_attribute del_thm;
-
-val setup =
-  Attrib.setup @{binding noatp} (Attrib.add_del add del) "sledgehammer blacklisting" #>
-  PureThy.add_thms_dynamic (@{binding noatp}, map #2 o Termtab.dest o Data.get);
-
-end;