src/Pure/library.ML
changeset 4792 8e3c2dddb9c8
parent 4713 bea2ab2e360b
child 4849 a9d5b8f8e40f
--- a/src/Pure/library.ML	Sat Apr 04 11:44:16 1998 +0200
+++ b/src/Pure/library.ML	Sat Apr 04 12:26:47 1998 +0200
@@ -234,6 +234,7 @@
   val scanwords: (string -> bool) -> string list -> string list
   datatype 'a mtree = Join of 'a * 'a mtree list
   type object
+  val type_error: string -> 'a
 end;
 
 structure Library: LIBRARY =
@@ -1004,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_msg " !! SYSTEM ERROR !!\n"; error 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 ();
@@ -1206,8 +1207,12 @@
 
 
 (* generic objects -- fool the ML type system via exception constructors *)
+
 type object = exn;
 
+fun type_error name =
+  error ("!! RUNTIME TYPE ERROR !!\nFailed to access " ^ quote name ^ " data");
+
 
 end;