# HG changeset patch
# User wenzelm
# Date 1120489634 -7200
# Node ID 34612070899858197c03c904e1831f5e48cb290d
# Parent  abd1461fa2880fc7bb2d6287e57d46a64fe03d70
tuned union: avoid garbage in trivial case;

diff -r abd1461fa288 -r 346120708998 src/Pure/General/ord_list.ML
--- a/src/Pure/General/ord_list.ML	Mon Jul 04 17:07:13 2005 +0200
+++ b/src/Pure/General/ord_list.ML	Mon Jul 04 17:07:14 2005 +0200
@@ -85,7 +85,10 @@
             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 subset ord (list1, list2) then list2
+    else handle_same (unio list1) list2
+  end;
 
 (*intersection: filter second list for elements present in first list*)
 nonfix inter;