src/Pure/item_net.ML

 signature ITEM_NET =
 sig
   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
   val remove: 'a -> 'a T -> 'a T
   val update: 'a -> 'a T -> 'a T

   Items {eq = eq, index = index, content = content, next = next, net = net};
 
 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;
 
 
 (* standard operations *)