removed type object (see object.ML);
authorwenzelm
Fri Jun 05 14:23:52 1998 +0200 (1998-06-05)
changeset 4995905cd6f73429
parent 4994 8b361563d470
child 4996 951575080635
removed type object (see object.ML);
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Fri Jun 05 14:23:27 1998 +0200
     1.2 +++ b/src/Pure/library.ML	Fri Jun 05 14:23:52 1998 +0200
     1.3 @@ -239,13 +239,12 @@
     1.4    val bump_string: string -> string
     1.5    val scanwords: (string -> bool) -> string list -> string list
     1.6    datatype 'a mtree = Join of 'a * 'a mtree list
     1.7 -  type object
     1.8 -  val type_error: string -> 'a
     1.9  end;
    1.10  
    1.11  structure Library: LIBRARY =
    1.12  struct
    1.13  
    1.14 +
    1.15  (** functions **)
    1.16  
    1.17  (*handy combinators*)
    1.18 @@ -1252,14 +1251,6 @@
    1.19  datatype 'a mtree = Join of 'a * 'a mtree list;
    1.20  
    1.21  
    1.22 -(* generic objects -- fool the ML type system via exception constructors *)
    1.23 -
    1.24 -type object = exn;
    1.25 -
    1.26 -fun type_error name =
    1.27 -  error ("## RUNTIME TYPE ERROR ##\nFailed to access " ^ quote name ^ " data");
    1.28 -
    1.29 -
    1.30  end;
    1.31  
    1.32  open Library;