1.1 --- a/src/Provers/classical.ML	Sat Apr 04 11:44:16 1998 +0200
     1.2 +++ b/src/Provers/classical.ML	Sat Apr 04 12:26:47 1998 +0200
     1.3 @@ -759,7 +759,7 @@
     1.4  fun claset_ref_of_sg sg =
     1.5    (case Sign.get_data sg clasetK of
     1.6      ClasetData (ref (CSData r)) => r
     1.7 -  | _ => sys_error "claset_ref_of_sg");
     1.8 +  | _ => type_error clasetK);
     1.9  
    1.10  val claset_ref_of = claset_ref_of_sg o sign_of;
    1.11  val claset_of_sg = ! o claset_ref_of_sg;

     2.1 --- a/src/Pure/attribute.ML	Sat Apr 04 11:44:16 1998 +0200
     2.2 +++ b/src/Pure/attribute.ML	Sat Apr 04 12:26:47 1998 +0200
     2.3 @@ -127,7 +127,7 @@
     2.4  fun get_attributes_sg sg =
     2.5    (case Sign.get_data sg attributesK of
     2.6      Attributes x => x
     2.7 -  | _ => sys_error "get_attributes_sg");
     2.8 +  | _ => type_error attributesK);
     2.9  
    2.10  val get_attributes = get_attributes_sg o Theory.sign_of;
    2.11  

     3.1 --- a/src/Pure/library.ML	Sat Apr 04 11:44:16 1998 +0200
     3.2 +++ b/src/Pure/library.ML	Sat Apr 04 12:26:47 1998 +0200
     3.3 @@ -234,6 +234,7 @@
     3.4    val scanwords: (string -> bool) -> string list -> string list
     3.5    datatype 'a mtree = Join of 'a * 'a mtree list
     3.6    type object
     3.7 +  val type_error: string -> 'a
     3.8  end;
     3.9  
    3.10  structure Library: LIBRARY =
    3.11 @@ -1004,7 +1005,7 @@
    3.12  exception ERROR;
    3.13  fun error_msg s = !error_fn s;	  (*promise to raise ERROR later!*)
    3.14  fun error s = (error_msg s; raise ERROR);
    3.15 -fun sys_error msg = (error_msg " !! SYSTEM ERROR !!\n"; error msg);
    3.16 +fun sys_error msg = error ("!! SYSTEM ERROR !!\n" ^ msg);
    3.17  
    3.18  fun assert p msg = if p then () else error msg;
    3.19  fun deny p msg = if p then error msg else ();
    3.20 @@ -1206,8 +1207,12 @@
    3.21  
    3.22  
    3.23  (* generic objects -- fool the ML type system via exception constructors *)
    3.24 +
    3.25  type object = exn;
    3.26  
    3.27 +fun type_error name =
    3.28 +  error ("!! RUNTIME TYPE ERROR !!\nFailed to access " ^ quote name ^ " data");
    3.29 +
    3.30  
    3.31  end;
    3.32  

     4.1 --- a/src/Pure/pure_thy.ML	Sat Apr 04 11:44:16 1998 +0200
     4.2 +++ b/src/Pure/pure_thy.ML	Sat Apr 04 12:26:47 1998 +0200
     4.3 @@ -86,7 +86,7 @@
     4.4  fun get_theorems_sg sg =
     4.5    (case Sign.get_data sg theoremsK of
     4.6      Theorems r => r
     4.7 -  | _ => sys_error "get_theorems_sg");
     4.8 +  | _ => type_error theoremsK);
     4.9  
    4.10  val get_theorems = get_theorems_sg o Theory.sign_of;
    4.11