--- a/src/Provers/classical.ML Sat Apr 04 11:44:16 1998 +0200
+++ b/src/Provers/classical.ML Sat Apr 04 12:26:47 1998 +0200
@@ -759,7 +759,7 @@
fun claset_ref_of_sg sg =
(case Sign.get_data sg clasetK of
ClasetData (ref (CSData r)) => r
- | _ => sys_error "claset_ref_of_sg");
+ | _ => type_error clasetK);
val claset_ref_of = claset_ref_of_sg o sign_of;
val claset_of_sg = ! o claset_ref_of_sg;
--- a/src/Pure/attribute.ML Sat Apr 04 11:44:16 1998 +0200
+++ b/src/Pure/attribute.ML Sat Apr 04 12:26:47 1998 +0200
@@ -127,7 +127,7 @@
fun get_attributes_sg sg =
(case Sign.get_data sg attributesK of
Attributes x => x
- | _ => sys_error "get_attributes_sg");
+ | _ => type_error attributesK);
val get_attributes = get_attributes_sg o Theory.sign_of;
--- 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;
--- a/src/Pure/pure_thy.ML Sat Apr 04 11:44:16 1998 +0200
+++ b/src/Pure/pure_thy.ML Sat Apr 04 12:26:47 1998 +0200
@@ -86,7 +86,7 @@
fun get_theorems_sg sg =
(case Sign.get_data sg theoremsK of
Theorems r => r
- | _ => sys_error "get_theorems_sg");
+ | _ => type_error theoremsK);
val get_theorems = get_theorems_sg o Theory.sign_of;