# HG changeset patch
# User wenzelm
# Date 880034839 -3600
# Node ID 63ab0616900bd58c1aec205be7049cd7aa56658a
# Parent  8ae7ace96c391870cf582de6fa6f76cb982283aa
added type object = exn;

diff -r 8ae7ace96c39 -r 63ab0616900b 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;