# HG changeset patch
# User wenzelm
# Date 757156498 -3600
# Node ID 0dd3a0a264cdd43e7ce36823d41063dbef544712
# Parent  b9f087b42a4445c9c5af1a2f791df546f129e864
added sys_error;

diff -r b9f087b42a44 -r 0dd3a0a264cd src/Pure/library.ML
--- a/src/Pure/library.ML	Wed Dec 22 19:01:27 1993 +0100
+++ b/src/Pure/library.ML	Wed Dec 29 10:14:58 1993 +0100
@@ -216,7 +216,8 @@
 
 (*Print error message and abort to top level*)
 exception ERROR;
-fun error (msg) = (writeln msg;  raise ERROR);
+fun error msg = (writeln msg; raise ERROR);
+fun sys_error msg = (writeln "-- System Error --"; error msg);
 
 fun assert p msg = if p then () else error msg;
 fun deny p msg = if p then error msg else ();