tuned union: avoid garbage in trivial case;

--- 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;