--- a/src/Pure/library.ML Wed Apr 29 11:22:01 1998 +0200
+++ b/src/Pure/library.ML Wed Apr 29 11:22:52 1998 +0200
@@ -1005,7 +1005,7 @@
exception ERROR;
fun error_msg s = !error_fn s; (*promise to raise ERROR later!*)
fun error s = (error_msg s; raise ERROR);
-fun sys_error msg = error ("!! SYSTEM ERROR !!\n" ^ msg);
+fun sys_error msg = error ("## SYSTEM ERROR ##\n" ^ msg);
fun assert p msg = if p then () else error msg;
fun deny p msg = if p then error msg else ();
@@ -1211,7 +1211,7 @@
type object = exn;
fun type_error name =
- error ("!! RUNTIME TYPE ERROR !!\nFailed to access " ^ quote name ^ " data");
+ error ("## RUNTIME TYPE ERROR ##\nFailed to access " ^ quote name ^ " data");
end;