src/Pure/item_net.ML
changeset 36296 5cc547abd995
parent 33721 f15c9ded9676
child 42810 2425068fe13a
     1.1 --- a/src/Pure/item_net.ML	Fri Apr 23 16:12:57 2010 +0200
     1.2 +++ b/src/Pure/item_net.ML	Fri Apr 23 18:30:01 2010 +0200
     1.3 @@ -11,6 +11,7 @@
     1.4    val init: ('a * 'a -> bool) -> ('a -> term list) -> 'a T
     1.5    val content: 'a T -> 'a list
     1.6    val retrieve: 'a T -> term -> 'a list
     1.7 +  val member: 'a T -> 'a -> bool
     1.8    val merge: 'a T * 'a T -> 'a T
     1.9    val remove: 'a -> 'a T -> 'a T
    1.10    val update: 'a -> 'a T -> 'a T
    1.11 @@ -49,7 +50,6 @@
    1.12    mk_items eq index (x :: content) (next - 1)
    1.13      (fold (fn t => Net.insert_term (K false) (t, (next, x))) (index x) net);
    1.14  
    1.15 -
    1.16  fun merge (items1, Items {content = content2, ...}) =
    1.17    fold_rev (fn y => if member items1 y then I else cons y) content2 items1;
    1.18