--- a/src/Pure/General/table.ML Sat Jun 18 22:41:18 2005 +0200
+++ b/src/Pure/General/table.ML Sat Jun 18 22:42:01 2005 +0200
@@ -42,6 +42,7 @@
val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table (*exception DUPS*)
val delete: key -> 'a table -> 'a table (*exception UNDEF*)
val delete_safe: key -> 'a table -> 'a table
+ val member: ('b * 'a -> bool) -> 'a table -> key * 'b -> bool
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_multi: 'a list table * key -> 'a list
@@ -292,7 +293,12 @@
end;
-(* insert and remove *)
+(* member, insert and remove *)
+
+fun member eq tab (key, x) =
+ (case lookup (tab, key) of
+ NONE => false
+ | SOME y => eq (x, y));
fun insert eq (key, x) =
modify key (fn NONE => x | SOME y => if eq (x, y) then raise SAME else raise DUP key);