src/Pure/library.ML
changeset 3365 86c0d1988622
parent 3246 7f783705c7a4
child 3393 e31ac367387e
     1.1 --- a/src/Pure/library.ML	Tue May 27 17:49:52 1997 +0200
     1.2 +++ b/src/Pure/library.ML	Fri May 30 15:14:59 1997 +0200
     1.3 @@ -747,7 +747,9 @@
     1.4  		            (TextIO.stdOut, "\n*** " ^ s ^ "\n\n"));
     1.5  
     1.6  exception ERROR;
     1.7 -fun error msg = (!error_fn msg; raise ERROR);
     1.8 +fun error msg = (!error_fn msg;
     1.9 +		 TextIO.flushOut TextIO.stdOut; 
    1.10 +		 raise ERROR);
    1.11  fun sys_error msg = (!error_fn "*** SYSTEM ERROR ***"; error msg);
    1.12  
    1.13  fun assert p msg = if p then () else error msg;