--- a/src/Pure/codegen.ML Tue Feb 21 16:37:54 2006 +0100
+++ b/src/Pure/codegen.ML Wed Feb 22 10:18:17 2006 +0100
@@ -225,12 +225,12 @@
{codegens = codegens2, tycodegens = tycodegens2,
consts = consts2, types = types2, attrs = attrs2,
preprocs = preprocs2, modules = modules2, test_params = test_params2}) =
- {codegens = merge_alists' codegens1 codegens2,
- tycodegens = merge_alists' tycodegens1 tycodegens2,
+ {codegens = AList.merge (op =) (K true) (codegens1, codegens2),
+ tycodegens = AList.merge (op =) (K true) (tycodegens1, tycodegens2),
consts = merge_alists consts1 consts2,
types = merge_alists types1 types2,
attrs = merge_alists attrs1 attrs2,
- preprocs = merge_alists' preprocs1 preprocs2,
+ preprocs = AList.merge (op =) (K true) (preprocs1, preprocs2),
modules = Symtab.merge (K true) (modules1, modules2),
test_params = merge_test_params test_params1 test_params2};
--- a/src/Pure/library.ML Tue Feb 21 16:37:54 2006 +0100
+++ b/src/Pure/library.ML Wed Feb 22 10:18:17 2006 +0100
@@ -221,11 +221,8 @@
(*lists as tables -- see also Pure/General/alist.ML*)
val gen_merge_lists: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list
- val gen_merge_lists': ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list
val merge_lists: ''a list -> ''a list -> ''a list
- val merge_lists': ''a list -> ''a list -> ''a list
val merge_alists: (''a * 'b) list -> (''a * 'b) list -> (''a * 'b) list
- val merge_alists': (''a * 'b) list -> (''a * 'b) list -> (''a * 'b) list
(*balanced trees*)
exception Balance
@@ -1043,24 +1040,14 @@
in dups end;
-
-(** association lists **)
-
-(* lists as tables -- legacy operations *)
+(** association lists -- legacy operations **)
fun gen_merge_lists _ xs [] = xs
| gen_merge_lists _ [] ys = ys
| gen_merge_lists eq xs ys = xs @ gen_rems eq (ys, xs);
-fun gen_merge_lists' _ xs [] = xs
- | gen_merge_lists' _ [] 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;
fun merge_alists al = gen_merge_lists (eq_fst (op =)) al;
-fun merge_alists' al = gen_merge_lists' (eq_fst (op =)) al;
-
(** balanced trees **)