# HG changeset patch
# User wenzelm
# Date 1272040201 -7200
# Node ID 5cc547abd995d1bd94d8bba753f522ef9aab0f55
# Parent  9eaaa05c972c14ac94605bd0192c79d80e2841da
Item_Net/Named_Thms: export efficient member operation;

diff -r 9eaaa05c972c -r 5cc547abd995 src/Pure/Tools/named_thms.ML
--- a/src/Pure/Tools/named_thms.ML	Fri Apr 23 16:12:57 2010 +0200
+++ b/src/Pure/Tools/named_thms.ML	Fri Apr 23 18:30:01 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 9eaaa05c972c -r 5cc547abd995 src/Pure/item_net.ML
--- a/src/Pure/item_net.ML	Fri Apr 23 16:12:57 2010 +0200
+++ b/src/Pure/item_net.ML	Fri Apr 23 18:30:01 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;