# HG changeset patch
# User wenzelm
# Date 897049432 -7200
# Node ID 905cd6f73429af9c2bbee154ff3049277cf49eb6
# Parent  8b361563d4703f38291fe5e3023473b878cea574
removed type object (see object.ML);

diff -r 8b361563d470 -r 905cd6f73429 src/Pure/library.ML
--- a/src/Pure/library.ML	Fri Jun 05 14:23:27 1998 +0200
+++ b/src/Pure/library.ML	Fri Jun 05 14:23:52 1998 +0200
@@ -239,13 +239,12 @@
   val bump_string: string -> string
   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 =
 struct
 
+
 (** functions **)
 
 (*handy combinators*)
@@ -1252,14 +1251,6 @@
 datatype 'a mtree = Join of 'a * 'a mtree list;
 
 
-(* 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;
 
 open Library;