src/Pure/item_net.ML

--- a/src/Pure/item_net.ML	Wed Jan 13 15:17:11 2016 +0100
+++ b/src/Pure/item_net.ML	Wed Jan 13 15:58:39 2016 +0100
@@ -18,6 +18,7 @@
   val merge: 'a T * 'a T -> 'a T
   val remove: 'a -> 'a T -> 'a T
   val update: 'a -> 'a T -> 'a T
+  val filter: ('a -> bool) -> 'a T -> 'a T
 end;
 
 structure Item_Net: ITEM_NET =
@@ -76,4 +77,7 @@
 
 fun update x items = cons x (remove x items);
 
+fun filter pred items =
+  fold (fn x => not (pred x) ? remove x) (content items) items;
+
 end;