# HG changeset patch
# User ballarin
# Date 1237411043 -3600
# Node ID ac50e7dedf6d2b5f32182f18a23f17839162d02d
# Parent  cc5a55d7a5be58cb64cda1fc62bc4215870795cd# Parent  8fbc355100f2ffc29ff8e7b98b5a10584f18881a
Merged.

diff -r cc5a55d7a5be -r ac50e7dedf6d src/Pure/General/ord_list.ML
--- a/src/Pure/General/ord_list.ML	Wed Mar 18 22:14:58 2009 +0100
+++ b/src/Pure/General/ord_list.ML	Wed Mar 18 22:17:23 2009 +0100
@@ -85,7 +85,7 @@
             LESS => x :: handle_same (unio xs) lst2
           | EQUAL => y :: unio xs ys
           | GREATER => y :: unio lst1 ys);
-  in handle_same (unio list1) list2 end;
+  in if pointer_eq (list1, list2) then list1 else handle_same (unio list1) list2 end;
 
 (*intersection: filter second list for elements present in first list*)
 nonfix inter;
diff -r cc5a55d7a5be -r ac50e7dedf6d src/Pure/library.ML
--- a/src/Pure/library.ML	Wed Mar 18 22:14:58 2009 +0100
+++ b/src/Pure/library.ML	Wed Mar 18 22:17:23 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 *)