diff -r 1ef2f0af7f26 -r 77da3aad5917 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Wed May 20 10:37:37 2009 +0200
+++ b/src/Pure/General/table.ML	Wed May 20 10:37:38 2009 +0200
@@ -33,11 +33,11 @@
   val max_key: 'a table -> key option
   val defined: 'a table -> key -> bool
   val lookup: 'a table -> key -> 'a option
-  val update: (key * 'a) -> 'a table -> 'a table
-  val update_new: (key * 'a) -> 'a table -> 'a table                   (*exception DUP*)
+  val update: key * 'a -> 'a table -> 'a table
+  val update_new: key * 'a -> 'a table -> 'a table                     (*exception DUP*)
   val default: key * 'a -> 'a table -> 'a table
   val map_entry: key -> ('a -> 'a) -> 'a table -> 'a table
-  val map_default: (key * 'a) -> ('a -> 'a) -> 'a table -> 'a table
+  val map_default: key * 'a -> ('a -> 'a) -> 'a table -> 'a table
   val make: (key * 'a) list -> 'a table                                (*exception DUP*)
   val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) ->
     'a table * 'a table -> 'a table                                    (*exception DUP*)
@@ -48,7 +48,7 @@
   val insert: ('a * 'a -> bool) -> key * 'a -> 'a table -> 'a table    (*exception DUP*)
   val remove: ('b * 'a -> bool) -> key * 'b -> 'a table -> 'a table
   val lookup_list: 'a list table -> key -> 'a list
-  val cons_list: (key * 'a) -> 'a list table -> 'a list table
+  val cons_list: key * 'a -> 'a list table -> 'a list table
   val insert_list: ('a * 'a -> bool) -> key * 'a -> 'a list table -> 'a list table
   val remove_list: ('b * 'a -> bool) -> key * 'b -> 'a list table -> 'a list table
   val update_list: ('a * 'a -> bool) -> key * 'a -> 'a list table -> 'a list table