flushOut ensures that no recent error message are lost (not certain this is
necessary)

--- a/src/Pure/library.ML	Tue May 27 17:49:52 1997 +0200
+++ b/src/Pure/library.ML	Fri May 30 15:14:59 1997 +0200
@@ -747,7 +747,9 @@
 		            (TextIO.stdOut, "\n*** " ^ s ^ "\n\n"));
 
 exception ERROR;
-fun error msg = (!error_fn msg; raise ERROR);
+fun error msg = (!error_fn msg;
+		 TextIO.flushOut TextIO.stdOut; 
+		 raise ERROR);
 fun sys_error msg = (!error_fn "*** SYSTEM ERROR ***"; error msg);
 
 fun assert p msg = if p then () else error msg;