# HG changeset patch
# User wenzelm
# Date 1006793302 -3600
# Node ID 83f747db967cb677f4e2b680619e69ae656a4b13
# Parent  2ef49890aede28ec66d756298ce7a403c240cc01
clarified order in gen_merge_lists';

diff -r 2ef49890aede -r 83f747db967c src/Pure/library.ML
--- 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;