--- 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;