# HG changeset patch
# User wenzelm
# Date 1525871070 -7200
# Node ID 5da8b97d9183c7ce5d99b0957b3dfb6f7cef5871
# Parent  2e5b737810a60a9f504f9c7f4168b3433d71a9c4
proper merge of items without term index (amending b969263fcf02);

diff -r 2e5b737810a6 -r 5da8b97d9183 src/Pure/item_net.ML
--- a/src/Pure/item_net.ML	Wed May 09 07:48:54 2018 +0200
+++ b/src/Pure/item_net.ML	Wed May 09 15:04:30 2018 +0200
@@ -9,6 +9,7 @@
 sig
   type 'a T
   val init: ('a * 'a -> bool) -> ('a -> term list) -> 'a T
+  val is_empty: 'a T -> bool
   val content: 'a T -> 'a list
   val length: 'a T -> int
   val retrieve: 'a T -> term -> 'a list
@@ -38,6 +39,7 @@
   Items {eq = eq, index = index, content = content, next = next, net = net};
 
 fun init eq index = mk_items eq index [] ~1 Net.empty;
+fun is_empty (Items {content, ...}) = null content;
 
 fun content (Items {content, ...}) = content;
 fun length items = List.length (content items);
@@ -62,12 +64,10 @@
   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 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 merge (items1, items2) =
+  if pointer_eq (items1, items2) then items1
+  else if is_empty items1 then items2
+  else fold_rev (fn y => if member items1 y then I else cons y) (content items2) items1;
 
 fun remove x (items as Items {eq, index, content, next, net}) =
   if member items x then