# HG changeset patch
# User berghofe
# Date 1098801215 -7200
# Node ID b40e91201039cdcaeeae29f4392b48af923f2f43
# Parent  49f70168f4c0a913cbc66ea0b0e868f83f0c6890
Added function merge_alists'.

diff -r 49f70168f4c0 -r b40e91201039 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;