separate ResBlacklist, based on scalable persistent data -- avoids inefficient hashing later on;

--- a/src/HOL/HOL.thy	Thu Oct 29 16:05:51 2009 +0100
+++ b/src/HOL/HOL.thy	Thu Oct 29 16:06:15 2009 +0100
@@ -24,6 +24,7 @@
   "~~/src/Tools/coherent.ML"
   "~~/src/Tools/eqsubst.ML"
   "~~/src/Provers/quantifier1.ML"
+  "Tools/res_blacklist.ML"
   ("Tools/simpdata.ML")
   "~~/src/Tools/random_word.ML"
   "~~/src/Tools/atomize_elim.ML"
@@ -34,6 +35,7 @@
 begin
 
 setup {* Intuitionistic.method_setup @{binding iprover} *}
+setup ResBlacklist.setup
 
 
 subsection {* Primitive logic *}
@@ -833,19 +835,14 @@
   val hyp_subst_tacs = [Hypsubst.hyp_subst_tac]
 end);
 
-structure BasicClassical: BASIC_CLASSICAL = Classical; 
-open BasicClassical;
+structure Basic_Classical: BASIC_CLASSICAL = Classical; 
+open Basic_Classical;
 
 ML_Antiquote.value "claset"
   (Scan.succeed "Classical.claset_of (ML_Context.the_local_context ())");
-
-structure ResBlacklist = Named_Thms
-  (val name = "noatp" val description = "theorems blacklisted for ATP");
 *}
 
-text {*ResBlacklist holds 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.*}
+setup Classical.setup
 
 setup {*
 let
@@ -856,8 +853,6 @@
 in
   Hypsubst.hypsubst_setup
   #> ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)
-  #> Classical.setup
-  #> ResBlacklist.setup
 end
 *}
 

--- a/src/HOL/IsaMakefile	Thu Oct 29 16:05:51 2009 +0100
+++ b/src/HOL/IsaMakefile	Thu Oct 29 16:06:15 2009 +0100
@@ -302,6 +302,7 @@
   Tools/choice_specification.ML \
   Tools/res_atp.ML \
   Tools/res_axioms.ML \
+  Tools/res_blacklist.ML \
   Tools/res_clause.ML \
   Tools/res_hol_clause.ML \
   Tools/res_reconstruct.ML \

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/res_blacklist.ML	Thu Oct 29 16:06:15 2009 +0100
@@ -0,0 +1,43 @@
+(*  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 ResBlacklist: RES_BLACKLIST =
+struct
+
+structure Data = GenericDataFun
+(
+  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;