--- a/src/Pure/General/table.ML Thu Jun 02 18:29:51 2005 +0200
+++ b/src/Pure/General/table.ML Thu Jun 02 18:29:52 2005 +0200
@@ -28,6 +28,7 @@
val min_key: 'a table -> key option
val max_key: 'a table -> key option
val exists: (key * 'a -> bool) -> 'a table -> bool
+ val forall: (key * 'a -> bool) -> 'a table -> 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*)
@@ -92,7 +93,16 @@
fun dest tab = rev (foldl_table (fn (rev_ps, p) => p :: rev_ps) ([], tab));
fun keys tab = rev (foldl_table (fn (rev_ks, (k, _)) => k :: rev_ks) ([], tab));
-fun exists P tab = foldl_table (fn (false, e) => P e | (b, _) => b) (false, tab);
+
+local exception TRUE in
+
+fun exists pred tab =
+ (foldl_table (fn ((), e) => if pred e then raise TRUE else ()) ((), tab); false)
+ handle TRUE => true;
+
+fun forall pred = not o exists (not o pred);
+
+end;
fun min_key Empty = NONE
| min_key (Branch2 (left, (k, _), _)) = SOME (if_none (min_key left) k)