src/Pure/item_net.ML

--- a/src/Pure/item_net.ML	Sat May 14 18:29:06 2011 +0200
+++ b/src/Pure/item_net.ML	Sat May 14 21:42:17 2011 +0200
@@ -10,6 +10,7 @@
   type 'a T
   val init: ('a * 'a -> bool) -> ('a -> term list) -> 'a T
   val content: 'a T -> 'a list
+  val length: 'a T -> int
   val retrieve: 'a T -> term -> 'a list
   val member: 'a T -> 'a -> bool
   val merge: 'a T * 'a T -> 'a T
@@ -36,6 +37,7 @@
 fun init eq index = mk_items eq index [] ~1 Net.empty;
 
 fun content (Items {content, ...}) = content;
+fun length items = List.length (content items);
 fun retrieve (Items {net, ...}) = order_list o Net.unify_term net;