abandoned merge_alists' in favour of generic AList.merge
authorhaftmann
Wed Feb 22 10:18:17 2006 +0100 (2006-02-22)
changeset 19119dea8d858d37f
parent 19118 52f751b50716
child 19120 353d349740de
abandoned merge_alists' in favour of generic AList.merge
src/Pure/codegen.ML
src/Pure/library.ML
     1.1 --- a/src/Pure/codegen.ML	Tue Feb 21 16:37:54 2006 +0100
     1.2 +++ b/src/Pure/codegen.ML	Wed Feb 22 10:18:17 2006 +0100
     1.3 @@ -225,12 +225,12 @@
     1.4       {codegens = codegens2, tycodegens = tycodegens2,
     1.5        consts = consts2, types = types2, attrs = attrs2,
     1.6        preprocs = preprocs2, modules = modules2, test_params = test_params2}) =
     1.7 -    {codegens = merge_alists' codegens1 codegens2,
     1.8 -     tycodegens = merge_alists' tycodegens1 tycodegens2,
     1.9 +    {codegens = AList.merge (op =) (K true) (codegens1, codegens2),
    1.10 +     tycodegens = AList.merge (op =) (K true) (tycodegens1, tycodegens2),
    1.11       consts = merge_alists consts1 consts2,
    1.12       types = merge_alists types1 types2,
    1.13       attrs = merge_alists attrs1 attrs2,
    1.14 -     preprocs = merge_alists' preprocs1 preprocs2,
    1.15 +     preprocs = AList.merge (op =) (K true) (preprocs1, preprocs2),
    1.16       modules = Symtab.merge (K true) (modules1, modules2),
    1.17       test_params = merge_test_params test_params1 test_params2};
    1.18  
     2.1 --- a/src/Pure/library.ML	Tue Feb 21 16:37:54 2006 +0100
     2.2 +++ b/src/Pure/library.ML	Wed Feb 22 10:18:17 2006 +0100
     2.3 @@ -221,11 +221,8 @@
     2.4  
     2.5    (*lists as tables -- see also Pure/General/alist.ML*)
     2.6    val gen_merge_lists: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list
     2.7 -  val gen_merge_lists': ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list
     2.8    val merge_lists: ''a list -> ''a list -> ''a list
     2.9 -  val merge_lists': ''a list -> ''a list -> ''a list
    2.10    val merge_alists: (''a * 'b) list -> (''a * 'b) list -> (''a * 'b) list
    2.11 -  val merge_alists': (''a * 'b) list -> (''a * 'b) list -> (''a * 'b) list
    2.12  
    2.13    (*balanced trees*)
    2.14    exception Balance
    2.15 @@ -1043,24 +1040,14 @@
    2.16    in dups end;
    2.17  
    2.18  
    2.19 -
    2.20 -(** association lists **)
    2.21 -
    2.22 -(* lists as tables -- legacy operations *)
    2.23 +(** association lists -- legacy operations **)
    2.24  
    2.25  fun gen_merge_lists _ xs [] = xs
    2.26    | gen_merge_lists _ [] ys = ys
    2.27    | gen_merge_lists eq xs ys = xs @ gen_rems eq (ys, xs);
    2.28  
    2.29 -fun gen_merge_lists' _ xs [] = xs
    2.30 -  | gen_merge_lists' _ [] ys = ys
    2.31 -  | gen_merge_lists' eq xs ys = gen_rems eq (ys, xs) @ xs;
    2.32 -
    2.33  fun merge_lists xs ys = gen_merge_lists (op =) xs ys;
    2.34 -fun merge_lists' xs ys = gen_merge_lists' (op =) xs ys;
    2.35  fun merge_alists al = gen_merge_lists (eq_fst (op =)) al;
    2.36 -fun merge_alists' al = gen_merge_lists' (eq_fst (op =)) al;
    2.37 -
    2.38  
    2.39  
    2.40  (** balanced trees **)