# HG changeset patch
# User wenzelm
# Date 1117729792 -7200
# Node ID 733267a60e322a5f329d634659b98e9d564c3a7b
# Parent  9d503d6fcbb1d5127f3395f41a71ce30d023b966
exists: made non-strict;
added forall;

diff -r 9d503d6fcbb1 -r 733267a60e32 src/Pure/General/table.ML
--- 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)