diff -r c12484a27367 -r 8fbc355100f2 src/Pure/library.ML
--- a/src/Pure/library.ML	Wed Mar 18 19:11:26 2009 +0100
+++ b/src/Pure/library.ML	Wed Mar 18 20:03:01 2009 +0100
@@ -817,8 +817,10 @@
 
 fun subtract eq = fold (remove eq);
 
-fun merge _ ([], ys) = ys
-  | merge eq (xs, ys) = fold_rev (insert eq) ys xs;
+fun merge eq (xs, ys) =
+  if pointer_eq (xs, ys) then xs
+  else if null xs then ys
+  else fold_rev (insert eq) ys xs;
 
 
 (* old-style infixes *)