# HG changeset patch
# User wenzelm
# Date 891685607 -7200
# Node ID 8e3c2dddb9c8b2186888e7e3263c3d77aee17f8a
# Parent  0cc16c8133bb8590dfa3a4998c220df41752bf5d
type_error;

diff -r 0cc16c8133bb -r 8e3c2dddb9c8 src/Provers/classical.ML
--- 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;
diff -r 0cc16c8133bb -r 8e3c2dddb9c8 src/Pure/attribute.ML
--- 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;
 
diff -r 0cc16c8133bb -r 8e3c2dddb9c8 src/Pure/library.ML
--- 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;
 
diff -r 0cc16c8133bb -r 8e3c2dddb9c8 src/Pure/pure_thy.ML
--- 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;