Added function merge_alists'.
authorberghofe
Tue, 26 Oct 2004 16:33:35 +0200
changeset 15263 b40e91201039
parent 15262 49f70168f4c0
child 15264 a881ad2e9edc
Added function merge_alists'.
src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Oct 26 16:33:09 2004 +0200
+++ b/src/Pure/library.ML	Tue Oct 26 16:33:35 2004 +0200
@@ -230,6 +230,7 @@
   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
@@ -1072,6 +1073,7 @@
 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 al;
+fun merge_alists' al = gen_merge_lists' eq_fst al;