--- 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;