--- a/src/Pure/library.ML Sat Nov 24 17:21:47 2001 +0100
+++ b/src/Pure/library.ML Mon Nov 26 17:48:22 2001 +0100
@@ -914,8 +914,7 @@
(*removing an element from a list -- possibly WITH duplicates*)
fun gen_rem eq (xs, y) = filter_out (fn x => eq (x, y)) xs;
-
-fun gen_rems eq = foldl (gen_rem eq);
+fun gen_rems eq (xs, ys) = filter_out (fn x => gen_mem eq (x, ys)) xs;
(*makes a list of the distinct members of the input; preserves order, takes
@@ -1019,7 +1018,7 @@
fun gen_merge_lists' _ xs [] = xs
| gen_merge_lists' _ [] ys = ys
- | gen_merge_lists' eq xs ys = gen_rems eq (xs, ys) @ ys;
+ | gen_merge_lists' eq xs ys = gen_rems eq (ys, xs) @ xs;
fun merge_lists xs ys = gen_merge_lists (op =) xs ys;
fun merge_lists' xs ys = gen_merge_lists' (op =) xs ys;