src/Pure/General/ord_list.ML
changeset 16886 7328996728a6
parent 16811 23b9c52612db
child 22364 ddb91c9eb0fc
     1.1 --- a/src/Pure/General/ord_list.ML	Tue Jul 19 17:21:57 2005 +0200
     1.2 +++ b/src/Pure/General/ord_list.ML	Tue Jul 19 17:21:58 2005 +0200
     1.3 @@ -84,10 +84,7 @@
     1.4              LESS => x :: handle_same (unio xs) lst2
     1.5            | EQUAL => y :: unio xs ys
     1.6            | GREATER => y :: unio lst1 ys);
     1.7 -  in
     1.8 -    if subset ord (list1, list2) then list2
     1.9 -    else handle_same (unio list1) list2
    1.10 -  end;
    1.11 +  in handle_same (unio list1) list2 end;
    1.12  
    1.13  (*intersection: filter second list for elements present in first list*)
    1.14  nonfix inter;