tuned signature;

--- a/src/HOL/Eisbach/match_method.ML	Wed Jan 13 15:17:11 2016 +0100
+++ b/src/HOL/Eisbach/match_method.ML	Wed Jan 13 15:58:39 2016 +0100
@@ -34,10 +34,6 @@
   end;
 
 
-fun Item_Net_filter f net =
-  fold (fn item => not (f item) ? Item_Net.remove item) (Item_Net.content net) net
-
-
 datatype match_kind =
     Match_Term of term Item_Net.T
   | Match_Fact of thm Item_Net.T
@@ -686,14 +682,14 @@
                 val (_, after_prems) = focus_prems inner_ctxt;
 
                 val removed_prems =
-                  Item_Net_filter (null o Item_Net.lookup after_prems) before_prems
+                  Item_Net.filter (null o Item_Net.lookup after_prems) before_prems
 
                 val removed_local_prems = Item_Net.content removed_prems
                   |> filter (fn (id, _) => member (op =) local_premids id)
                   |> map (fn (_, prem) => Thm.prop_of prem)
 
                 fun filter_removed_prems prems =
-                  Item_Net_filter (null o Item_Net.lookup removed_prems) prems;
+                  Item_Net.filter (null o Item_Net.lookup removed_prems) prems;
                                      
                 val outer_ctxt' = outer_ctxt 
                   |> Focus_Data.map (@{apply 3(1)} (apsnd filter_removed_prems));

--- 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;