removed obsolete Named_Thm_Set -- Named_Thms provides efficient member operation;

--- a/src/HOL/HOL.thy	Fri Apr 23 18:30:01 2010 +0200
+++ b/src/HOL/HOL.thy	Fri Apr 23 19:36:04 2010 +0200
@@ -30,7 +30,6 @@
   ("~~/src/Tools/induct_tacs.ML")
   ("Tools/recfun_codegen.ML")
   "~~/src/Tools/more_conv.ML"
-  "~~/src/HOL/Tools/Sledgehammer/named_thm_set.ML"
 begin
 
 setup {* Intuitionistic.method_setup @{binding iprover} *}
@@ -801,7 +800,7 @@
 *}
 
 ML {*
-structure No_ATPs = Named_Thm_Set
+structure No_ATPs = Named_Thms
 (
   val name = "no_atp"
   val description = "theorems that should be filtered out by Sledgehammer"

--- a/src/HOL/IsaMakefile	Fri Apr 23 18:30:01 2010 +0200
+++ b/src/HOL/IsaMakefile	Fri Apr 23 19:36:04 2010 +0200
@@ -136,7 +136,6 @@
   $(SRC)/Tools/random_word.ML \
   $(SRC)/Tools/value.ML \
   HOL.thy \
-  Tools/Sledgehammer/named_thm_set.ML \
   Tools/hologic.ML \
   Tools/recfun_codegen.ML \
   Tools/simpdata.ML

--- a/src/HOL/Tools/Sledgehammer/named_thm_set.ML	Fri Apr 23 18:30:01 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,45 +0,0 @@
-(*  Title:      HOL/Tools/Sledgehammer/named_thm_set.ML
-    Author:     Makarius
-    Author:     Jasmin Blanchette, TU Muenchen
-
-Named sets of theorems.
-*)
-
-signature NAMED_THM_SET =
-sig
-  val member: Proof.context -> thm -> bool
-  val add_thm: thm -> Context.generic -> Context.generic
-  val del_thm: thm -> Context.generic -> Context.generic
-  val add: attribute
-  val del: attribute
-  val setup: theory -> theory
-end;
-
-functor Named_Thm_Set(val name: string val description: string)
-        : NAMED_THM_SET =
-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 member 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.name name) (Attrib.add_del add del)
-               ("declaration of " ^ description) #>
-  PureThy.add_thms_dynamic (Binding.name name,
-                            map #2 o Termtab.dest o Data.get);
-
-end;