# HG changeset patch
# User haftmann
# Date 1256223126 -7200
# Node ID 3aea60ca390012baa886d39bf08c8509c2284d99
# Parent  3c9cf88ec841256604190f94d88beb1775e60a74
multiset operations with canonical argument order

diff -r 3c9cf88ec841 -r 3aea60ca3900 src/Pure/library.ML
--- a/src/Pure/library.ML	Thu Oct 22 16:52:06 2009 +0200
+++ b/src/Pure/library.ML	Thu Oct 22 16:52:06 2009 +0200
@@ -173,7 +173,7 @@
 
   (*lists as multisets*)
   val remove1: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list
-  val submultiset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
+  val combine: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list
 
   (*orders*)
   val is_equal: order -> bool
@@ -858,11 +858,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 submultiset _ ([], _)  = true
-  | submultiset eq (x :: xs, ys) = member eq ys x andalso submultiset eq (xs, remove1 eq x ys);
+fun combine eq xs ys = fold (remove1 eq) ys xs @ ys;