src/Pure/library.ML
changeset 544 c53386a5bcf1
parent 512 55755ed9fab9
child 955 aa0c5f9daf5b
     1.1 --- a/src/Pure/library.ML	Thu Aug 18 17:41:40 1994 +0200
     1.2 +++ b/src/Pure/library.ML	Thu Aug 18 17:50:22 1994 +0200
     1.3 @@ -647,6 +647,12 @@
     1.4  fun assert p msg = if p then () else error msg;
     1.5  fun deny p msg = if p then error msg else ();
     1.6  
     1.7 +(*Assert pred for every member of l, generating a message if pred fails*)
     1.8 +fun assert_all pred l msg_fn = 
     1.9 +  let fun asl [] = ()
    1.10 +	| asl (x::xs) = if pred x then asl xs
    1.11 +	                else error (msg_fn x)
    1.12 +  in  asl l  end;
    1.13  
    1.14  (* FIXME close file (?) *)
    1.15  (*for the "test" target in Makefiles -- signifies successful termination*)