--- a/src/Pure/General/ord_list.ML Sat Jan 08 17:14:48 2011 +0100
+++ b/src/Pure/General/ord_list.ML Sat Jan 08 17:30:05 2011 +0100
@@ -14,6 +14,7 @@
val remove: ('b * 'a -> order) -> 'b -> 'a T -> 'a T
val subset: ('b * 'a -> order) -> 'b T * 'a T -> bool
val union: ('a * 'a -> order) -> 'a T -> 'a T -> 'a T
+ val merge: ('a * 'a -> order) -> 'a T * 'a T -> 'a T
val inter: ('b * 'a -> order) -> 'b T -> 'a T -> 'a T
val subtract: ('b * 'a -> order) -> 'b T -> 'a T -> 'a T
end;
@@ -85,6 +86,8 @@
| GREATER => y :: unio lst1 ys);
in if pointer_eq (list1, list2) then list1 else handle_same (unio list1) list2 end;
+fun merge ord (list1, list2) = union ord list2 list1;
+
(*intersection: filter second list for elements present in first list*)
fun inter ord list1 list2 =
let