# HG changeset patch
# User wenzelm
# Date 1393329188 -3600
# Node ID b969263fcf0236e26575ac13b2ca45646561c0f2
# Parent  11dd48f84441b5b01d2273d25d3a4f807be2e4a7
optimize special case according to Library.merge (see also 8fbc355100f2);
no treatment for Net.merge, due to non-standard merge order;

diff -r 11dd48f84441 -r b969263fcf02 src/Pure/item_net.ML
--- a/src/Pure/item_net.ML	Tue Feb 25 11:36:04 2014 +0100
+++ b/src/Pure/item_net.ML	Tue Feb 25 12:53:08 2014 +0100
@@ -54,8 +54,12 @@
   mk_items eq index (x :: content) (next - 1)
     (fold (fn t => Net.insert_term (K false) (t, (next, x))) (index x) net);
 
-fun merge (items1, Items {content = content2, ...}) =
-  fold_rev (fn y => if member items1 y then I else cons y) content2 items1;
+fun merge
+    (items1 as Items {net = net1, ...},
+     items2 as Items {net = net2, content = content2, ...}) =
+  if pointer_eq (net1, net2) then items1
+  else if Net.is_empty net1 then items2
+  else fold_rev (fn y => if member items1 y then I else cons y) content2 items1;
 
 fun remove x (items as Items {eq, index, content, next, net}) =
   if member items x then
diff -r 11dd48f84441 -r b969263fcf02 src/Pure/net.ML
--- a/src/Pure/net.ML	Tue Feb 25 11:36:04 2014 +0100
+++ b/src/Pure/net.ML	Tue Feb 25 12:53:08 2014 +0100
@@ -20,6 +20,7 @@
   val encode_type: typ -> term
   type 'a net
   val empty: 'a net
+  val is_empty: 'a net -> bool
   exception INSERT
   val insert: ('a * 'a -> bool) -> key list * 'a -> 'a net -> 'a net
   val insert_term: ('a * 'a -> bool) -> term * 'a -> 'a net -> 'a net
@@ -251,7 +252,8 @@
       map (cons_fst VarK) (dest var) @
       maps (fn (a, net) => map (cons_fst (AtomK a)) (dest net)) (Symtab.dest atoms);
 
-fun merge eq (net1, net2) = fold (insert_safe eq) (dest net2) net1;
+fun merge eq (net1, net2) =
+  fold (insert_safe eq) (dest net2) net1;  (* FIXME non-standard merge order!?! *)
 
 fun content net = map #2 (dest net);