# HG changeset patch
# User wenzelm
# Date 1452697177 -3600
# Node ID 3499ec79ad4b79f681d5867d55ab21de2813b797
# Parent  b10046b14dd878e91fdcd564244f750e5554c080# Parent  a12413bec743f6dc4f586f570b6e606db1e3472c
merged;

diff -r a12413bec743 -r 3499ec79ad4b NEWS
--- a/NEWS	Wed Jan 13 15:46:21 2016 +0100
+++ b/NEWS	Wed Jan 13 15:59:37 2016 +0100
@@ -50,9 +50,6 @@
 
 *** Prover IDE -- Isabelle/Scala/jEdit ***
 
-* Update to jedit-5.3.0, with improved GUI scaling and support of
-high-resolution displays (e.g. 4K).
-
 * IDE support for the source-level debugger of Poly/ML, to work with
 Isabelle/ML and official Standard ML. Configuration option "ML_debugger"
 and commands 'ML_file_debug', 'ML_file_no_debug', 'SML_file_debug',
@@ -114,6 +111,9 @@
 works better with GUI scaling for very high-resolution displays (e.g.
 4K). Moreover, it is generally more robust than "Nimbus".
 
+* Update to jedit-5.3.0, with improved GUI scaling and support of
+high-resolution displays (e.g. 4K).
+
 * The main Isabelle executable is managed as single-instance Desktop
 application uniformly on all platforms: Linux, Windows, Mac OS X.
 
diff -r a12413bec743 -r 3499ec79ad4b src/HOL/Eisbach/match_method.ML
--- a/src/HOL/Eisbach/match_method.ML	Wed Jan 13 15:46:21 2016 +0100
+++ b/src/HOL/Eisbach/match_method.ML	Wed Jan 13 15:59:37 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));
diff -r a12413bec743 -r 3499ec79ad4b src/Pure/item_net.ML
--- a/src/Pure/item_net.ML	Wed Jan 13 15:46:21 2016 +0100
+++ b/src/Pure/item_net.ML	Wed Jan 13 15:59:37 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;