# HG changeset patch
# User wenzelm
# Date 1119127321 -7200
# Node ID 82e2fc13ce5461dbea704f003951b6f7964ad5a1
# Parent  eb287ce972308b001f81a796dd1ba5a0193c7f39
added member;

diff -r eb287ce97230 -r 82e2fc13ce54 src/Pure/General/table.ML
--- 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);