# HG changeset patch
# User wenzelm
# Date 893841772 -7200
# Node ID a9d5b8f8e40f044ac12c1fa59f40441370302749
# Parent  99c8d95c51d613c1a97bb55002faba2d2c0c6dda
tuned error msgs;

diff -r 99c8d95c51d6 -r a9d5b8f8e40f src/Pure/library.ML
--- 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;