# HG changeset patch
# User lcp
# Date 777225022 -7200
# Node ID c53386a5bcf18d2903f6e00feec8c1c05111bb6a
# Parent  e961b2092869f9188f3fdbe6b04631a305df2971
Pure/library/assert_all: new, moved from ZF/ind_syntax.ML

diff -r e961b2092869 -r c53386a5bcf1 src/Pure/library.ML
--- a/src/Pure/library.ML	Thu Aug 18 17:41:40 1994 +0200
+++ b/src/Pure/library.ML	Thu Aug 18 17:50:22 1994 +0200
@@ -647,6 +647,12 @@
 fun assert p msg = if p then () else error msg;
 fun deny p msg = if p then error msg else ();
 
+(*Assert pred for every member of l, generating a message if pred fails*)
+fun assert_all pred l msg_fn = 
+  let fun asl [] = ()
+	| asl (x::xs) = if pred x then asl xs
+	                else error (msg_fn x)
+  in  asl l  end;
 
 (* FIXME close file (?) *)
 (*for the "test" target in Makefiles -- signifies successful termination*)