--- a/src/Pure/General/table.ML Tue Jul 19 17:21:58 2005 +0200
+++ b/src/Pure/General/table.ML Tue Jul 19 17:21:59 2005 +0200
@@ -31,6 +31,7 @@
val max_key: 'a table -> key option
val exists: (key * 'a -> bool) -> 'a table -> bool
val forall: (key * 'a -> bool) -> 'a table -> bool
+ 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*)
@@ -145,6 +146,8 @@
| EQUAL => SOME x2
| GREATER => lookup (right, key)));
+fun defined tab key = is_some (lookup (tab, key));
+
(* updates *)