added type object = exn;
authorwenzelm
Thu, 20 Nov 1997 15:07:19 +0100
changeset 4255 63ab0616900b
parent 4254 8ae7ace96c39
child 4256 e768c42069bb
added type object = exn;
src/Pure/library.ML
--- a/src/Pure/library.ML	Thu Nov 20 15:06:57 1997 +0100
+++ b/src/Pure/library.ML	Thu Nov 20 15:07:19 1997 +0100
@@ -976,6 +976,10 @@
 datatype 'a mtree = Join of 'a * 'a mtree list;
 
 
+(* generic objects -- fool the ML type system via exception constructors *)
+type object = exn;
+
+
 end;
 
 open Library;