src/Pure/library.ML
changeset 4255 63ab0616900b
parent 4248 5e8a31c41d44
child 4284 eb65491ae776
     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;