# HG changeset patch
# User wenzelm
# Date 1121786518 -7200
# Node ID 7328996728a6c7a5c5fdaa280272caa5ac870907
# Parent  cabcd33cde180e724290016b181c645dc29efcc7
simplified union;

diff -r cabcd33cde18 -r 7328996728a6 src/Pure/General/ord_list.ML
--- a/src/Pure/General/ord_list.ML	Tue Jul 19 17:21:57 2005 +0200
+++ b/src/Pure/General/ord_list.ML	Tue Jul 19 17:21:58 2005 +0200
@@ -84,10 +84,7 @@
             LESS => x :: handle_same (unio xs) lst2
           | EQUAL => y :: unio xs ys
           | GREATER => y :: unio lst1 ys);
-  in
-    if subset ord (list1, list2) then list2
-    else handle_same (unio list1) list2
-  end;
+  in handle_same (unio list1) list2 end;
 
 (*intersection: filter second list for elements present in first list*)
 nonfix inter;