# HG changeset patch
# User haftmann
# Date 1140599897 -3600
# Node ID dea8d858d37fbc224713e67a32ea189299f0bf7f
# Parent  52f751b50716807267f4ad4b3558990a54275023
abandoned merge_alists' in favour of generic AList.merge

diff -r 52f751b50716 -r dea8d858d37f src/Pure/codegen.ML
--- 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};
 
diff -r 52f751b50716 -r dea8d858d37f src/Pure/library.ML
--- 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 **)