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;