merge_list: no exception DUP here;

--- 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 =