# HG changeset patch
# User wenzelm
# Date 1117533210 -7200
# Node ID 21ce46ca61cc6521b063bb0694e7d65c34d64fb7
# Parent  727c5e32930e65517273e3b44af5555b7458c9ef
remove(_multi): generalized type;

diff -r 727c5e32930e -r 21ce46ca61cc src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Tue May 31 11:53:29 2005 +0200
+++ b/src/Pure/General/table.ML	Tue May 31 11:53:30 2005 +0200
@@ -39,10 +39,10 @@
   val delete: key -> 'a table -> 'a table                              (*exception UNDEF*)
   val delete_safe: key -> 'a table -> 'a table
   val insert: ('a * 'a -> bool) -> key * 'a -> 'a table -> 'a table    (*exception DUP*)
-  val remove: ('a * 'a -> bool) -> key * 'a -> 'a table -> 'a table
+  val remove: ('b * 'a -> bool) -> key * 'b -> 'a table -> 'a table
   val lookup_multi: 'a list table * key -> 'a list
   val update_multi: (key * 'a) * 'a list table -> 'a list table
-  val remove_multi: ('a * 'a -> bool) -> key * 'a -> 'a list table -> 'a list table
+  val remove_multi: ('b * 'a -> bool) -> key * 'b -> 'a list table -> 'a list table
   val make_multi: (key * 'a) list -> 'a list table
   val dest_multi: 'a list table -> (key * 'a) list
   val merge_multi: ('a * 'a -> bool) ->