tuned error msgs;
authorwenzelm
Wed, 29 Apr 1998 11:22:52 +0200
changeset 4849 a9d5b8f8e40f
parent 4848 99c8d95c51d6
child 4850 050481f41e28
tuned error msgs;
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;