# HG changeset patch
# User wenzelm
# Date 1272044183 -7200
# Node ID cf1abb4daae65dcd2c3c44d45a257f7ecc1b7691
# Parent  f2753d6b085908592e11abfd793c322512d5f718# Parent  6b2b9516a3cdeb30fef99237ca4064271ed03221
merged

diff -r f2753d6b0859 -r cf1abb4daae6 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Apr 23 19:32:37 2010 +0200
+++ b/src/HOL/HOL.thy	Fri Apr 23 19:36:23 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"
diff -r f2753d6b0859 -r cf1abb4daae6 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Apr 23 19:32:37 2010 +0200
+++ b/src/HOL/IsaMakefile	Fri Apr 23 19:36:23 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
diff -r f2753d6b0859 -r cf1abb4daae6 src/HOL/Tools/Sledgehammer/named_thm_set.ML
--- a/src/HOL/Tools/Sledgehammer/named_thm_set.ML	Fri Apr 23 19:32:37 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;
diff -r f2753d6b0859 -r cf1abb4daae6 src/Pure/Tools/named_thms.ML
--- a/src/Pure/Tools/named_thms.ML	Fri Apr 23 19:32:37 2010 +0200
+++ b/src/Pure/Tools/named_thms.ML	Fri Apr 23 19:36:23 2010 +0200
@@ -6,6 +6,7 @@
 
 signature NAMED_THMS =
 sig
+  val member: Proof.context -> thm -> bool
   val get: Proof.context -> thm list
   val add_thm: thm -> Context.generic -> Context.generic
   val del_thm: thm -> Context.generic -> Context.generic
@@ -25,6 +26,8 @@
   val merge = Item_Net.merge;
 );
 
+val member = Item_Net.member o Data.get o Context.Proof;
+
 val content = Item_Net.content o Data.get;
 val get = content o Context.Proof;
 
diff -r f2753d6b0859 -r cf1abb4daae6 src/Pure/item_net.ML
--- a/src/Pure/item_net.ML	Fri Apr 23 19:32:37 2010 +0200
+++ b/src/Pure/item_net.ML	Fri Apr 23 19:36:23 2010 +0200
@@ -11,6 +11,7 @@
   val init: ('a * 'a -> bool) -> ('a -> term list) -> 'a T
   val content: 'a T -> 'a list
   val retrieve: 'a T -> term -> 'a list
+  val member: 'a T -> 'a -> bool
   val merge: 'a T * 'a T -> 'a T
   val remove: 'a -> 'a T -> 'a T
   val update: 'a -> 'a T -> 'a T
@@ -49,7 +50,6 @@
   mk_items eq index (x :: content) (next - 1)
     (fold (fn t => Net.insert_term (K false) (t, (next, x))) (index x) net);
 
-
 fun merge (items1, Items {content = content2, ...}) =
   fold_rev (fn y => if member items1 y then I else cons y) content2 items1;