src/Pure/item_net.ML
changeset 55741 b969263fcf02
parent 53941 54874871aa06
child 59058 a78612c67ec0
     1.1 --- a/src/Pure/item_net.ML	Tue Feb 25 11:36:04 2014 +0100
     1.2 +++ b/src/Pure/item_net.ML	Tue Feb 25 12:53:08 2014 +0100
     1.3 @@ -54,8 +54,12 @@
     1.4    mk_items eq index (x :: content) (next - 1)
     1.5      (fold (fn t => Net.insert_term (K false) (t, (next, x))) (index x) net);
     1.6  
     1.7 -fun merge (items1, Items {content = content2, ...}) =
     1.8 -  fold_rev (fn y => if member items1 y then I else cons y) content2 items1;
     1.9 +fun merge
    1.10 +    (items1 as Items {net = net1, ...},
    1.11 +     items2 as Items {net = net2, content = content2, ...}) =
    1.12 +  if pointer_eq (net1, net2) then items1
    1.13 +  else if Net.is_empty net1 then items2
    1.14 +  else fold_rev (fn y => if member items1 y then I else cons y) content2 items1;
    1.15  
    1.16  fun remove x (items as Items {eq, index, content, next, net}) =
    1.17    if member items x then