clarified order in gen_merge_lists';
authorwenzelm
Mon Nov 26 17:48:22 2001 +0100 (2001-11-26)
changeset 1229583f747db967c
parent 12294 2ef49890aede
child 12296 45269a593e1b
clarified order in gen_merge_lists';
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Sat Nov 24 17:21:47 2001 +0100
     1.2 +++ b/src/Pure/library.ML	Mon Nov 26 17:48:22 2001 +0100
     1.3 @@ -914,8 +914,7 @@
     1.4  
     1.5  (*removing an element from a list -- possibly WITH duplicates*)
     1.6  fun gen_rem eq (xs, y) = filter_out (fn x => eq (x, y)) xs;
     1.7 -
     1.8 -fun gen_rems eq = foldl (gen_rem eq);
     1.9 +fun gen_rems eq (xs, ys) = filter_out (fn x => gen_mem eq (x, ys)) xs;
    1.10  
    1.11  
    1.12  (*makes a list of the distinct members of the input; preserves order, takes
    1.13 @@ -1019,7 +1018,7 @@
    1.14  
    1.15  fun gen_merge_lists' _ xs [] = xs
    1.16    | gen_merge_lists' _ [] ys = ys
    1.17 -  | gen_merge_lists' eq xs ys = gen_rems eq (xs, ys) @ ys;
    1.18 +  | gen_merge_lists' eq xs ys = gen_rems eq (ys, xs) @ xs;
    1.19  
    1.20  fun merge_lists xs ys = gen_merge_lists (op =) xs ys;
    1.21  fun merge_lists' xs ys = gen_merge_lists' (op =) xs ys;