--- a/src/Pure/library.ML Fri Oct 23 06:53:50 2009 +0200
+++ b/src/Pure/library.ML Fri Oct 23 10:11:56 2009 +0200
@@ -173,6 +173,7 @@
(*lists as multisets*)
val remove1: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list
+ val combine: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list
val submultiset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
(*orders*)
@@ -858,8 +859,10 @@
(** lists as multisets **)
-fun remove1 _ _ [] = raise Empty
- | remove1 eq y (x::xs) = if eq (y, x) then xs else x :: remove1 eq y xs;
+fun remove1 eq x [] = []
+ | remove1 eq x (y :: ys) = if eq (x, y) then ys else y :: remove1 eq x ys;
+
+fun combine eq xs ys = fold (remove1 eq) ys xs @ ys;
fun submultiset _ ([], _) = true
| submultiset eq (x :: xs, ys) = member eq ys x andalso submultiset eq (xs, remove1 eq x ys);