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