src/Pure/item_net.ML
changeset 42810 2425068fe13a
parent 36296 5cc547abd995
child 53941 54874871aa06
     1.1 --- a/src/Pure/item_net.ML	Sat May 14 18:29:06 2011 +0200
     1.2 +++ b/src/Pure/item_net.ML	Sat May 14 21:42:17 2011 +0200
     1.3 @@ -10,6 +10,7 @@
     1.4    type 'a T
     1.5    val init: ('a * 'a -> bool) -> ('a -> term list) -> 'a T
     1.6    val content: 'a T -> 'a list
     1.7 +  val length: 'a T -> int
     1.8    val retrieve: 'a T -> term -> 'a list
     1.9    val member: 'a T -> 'a -> bool
    1.10    val merge: 'a T * 'a T -> 'a T
    1.11 @@ -36,6 +37,7 @@
    1.12  fun init eq index = mk_items eq index [] ~1 Net.empty;
    1.13  
    1.14  fun content (Items {content, ...}) = content;
    1.15 +fun length items = List.length (content items);
    1.16  fun retrieve (Items {net, ...}) = order_list o Net.unify_term net;
    1.17  
    1.18