added type object = exn;
authorwenzelm
Thu Nov 20 15:07:19 1997 +0100 (1997-11-20)
changeset 425563ab0616900b
parent 4254 8ae7ace96c39
child 4256 e768c42069bb
added type object = exn;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Thu Nov 20 15:06:57 1997 +0100
     1.2 +++ b/src/Pure/library.ML	Thu Nov 20 15:07:19 1997 +0100
     1.3 @@ -976,6 +976,10 @@
     1.4  datatype 'a mtree = Join of 'a * 'a mtree list;
     1.5  
     1.6  
     1.7 +(* generic objects -- fool the ML type system via exception constructors *)
     1.8 +type object = exn;
     1.9 +
    1.10 +
    1.11  end;
    1.12  
    1.13  open Library;