src/Pure/library.ML
changeset 30572 8fbc355100f2
parent 30570 8fac7efcce0a
child 31250 4b99b1214034
     1.1 --- a/src/Pure/library.ML	Wed Mar 18 19:11:26 2009 +0100
     1.2 +++ b/src/Pure/library.ML	Wed Mar 18 20:03:01 2009 +0100
     1.3 @@ -817,8 +817,10 @@
     1.4  
     1.5  fun subtract eq = fold (remove eq);
     1.6  
     1.7 -fun merge _ ([], ys) = ys
     1.8 -  | merge eq (xs, ys) = fold_rev (insert eq) ys xs;
     1.9 +fun merge eq (xs, ys) =
    1.10 +  if pointer_eq (xs, ys) then xs
    1.11 +  else if null xs then ys
    1.12 +  else fold_rev (insert eq) ys xs;
    1.13  
    1.14  
    1.15  (* old-style infixes *)