# HG changeset patch
# User wenzelm
# Date 1256494451 -3600
# Node ID d11b89e7afd970c7b9db555b02faa1cab5531be2
# Parent  165a9f490d98d7dcefc5e8ece5dad7420bd0d0f8
merge_list: no exception DUP here;

diff -r 165a9f490d98 -r d11b89e7afd9 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Sun Oct 25 13:20:31 2009 +0100
+++ b/src/Pure/General/table.ML	Sun Oct 25 19:14:11 2009 +0100
@@ -54,8 +54,7 @@
   val update_list: ('a * 'a -> bool) -> key * 'a -> 'a list table -> 'a list table
   val make_list: (key * 'a) list -> 'a list table
   val dest_list: 'a list table -> (key * 'a) list
-  val merge_list: ('a * 'a -> bool) ->
-    'a list table * 'a list table -> 'a list table                     (*exception DUP*)
+  val merge_list: ('a * 'a -> bool) -> 'a list table * 'a list table -> 'a list table
 end;
 
 functor Table(Key: KEY): TABLE =