# HG changeset patch
# User wenzelm
# Date 1237402981 -3600
# Node ID 8fbc355100f2ffc29ff8e7b98b5a10584f18881a
# Parent  c12484a273678a840bf5c09447c87a034cfa8dc2
Library.merge/OrdList.union: optimize the important special case where the tables coincide -- NOTE: this changes both the operational behaviour and the result for non-standard eq/ord notion;

diff -r c12484a27367 -r 8fbc355100f2 src/Pure/General/ord_list.ML
--- a/src/Pure/General/ord_list.ML	Wed Mar 18 19:11:26 2009 +0100
+++ b/src/Pure/General/ord_list.ML	Wed Mar 18 20:03:01 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 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 *)