Added function merge_alists'.
authorberghofe
Tue Oct 26 16:33:35 2004 +0200 (2004-10-26)
changeset 15263b40e91201039
parent 15262 49f70168f4c0
child 15264 a881ad2e9edc
Added function merge_alists'.
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Tue Oct 26 16:33:09 2004 +0200
     1.2 +++ b/src/Pure/library.ML	Tue Oct 26 16:33:35 2004 +0200
     1.3 @@ -230,6 +230,7 @@
     1.4    val merge_lists: ''a list -> ''a list -> ''a list
     1.5    val merge_lists': ''a list -> ''a list -> ''a list
     1.6    val merge_alists: (''a * 'b) list -> (''a * 'b) list -> (''a * 'b) list
     1.7 +  val merge_alists': (''a * 'b) list -> (''a * 'b) list -> (''a * 'b) list
     1.8  
     1.9    (*balanced trees*)
    1.10    exception Balance
    1.11 @@ -1072,6 +1073,7 @@
    1.12  fun merge_lists xs ys = gen_merge_lists (op =) xs ys;
    1.13  fun merge_lists' xs ys = gen_merge_lists' (op =) xs ys;
    1.14  fun merge_alists al = gen_merge_lists eq_fst al;
    1.15 +fun merge_alists' al = gen_merge_lists' eq_fst al;
    1.16  
    1.17  
    1.18