# HG changeset patch
# User wenzelm
# Date 1121786519 -7200
# Node ID b24c067b32d671b0768c2c642b3f2b773d3ad3f1
# Parent  7328996728a6c7a5c5fdaa280272caa5ac870907
added defined;

diff -r 7328996728a6 -r b24c067b32d6 src/Pure/General/table.ML
--- 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 *)