# HG changeset patch
# User wenzelm
# Date 1119462080 -7200
# Node ID 86c9eada525bad3f1a5b51c90b93a75a14b3d894
# Parent  95460b6eb71267858147511bd5f1116edcafbf54
added structure Object (from Pure/General/object.ML);

diff -r 95460b6eb712 -r 86c9eada525b src/Pure/library.ML
--- a/src/Pure/library.ML	Wed Jun 22 19:41:19 2005 +0200
+++ b/src/Pure/library.ML	Wed Jun 22 19:41:20 2005 +0200
@@ -263,6 +263,7 @@
   val stamp: unit -> stamp
   type serial
   val serial: unit -> serial
+  structure Object: sig type T end
 end;
 
 signature LIBRARY =
@@ -1299,6 +1300,13 @@
 local val count = ref 0
 in fun serial () = inc count end;
 
+
+(* generic objects *)
+
+(*note that the builtin exception datatype may be extended by new
+  constructors at any time*)
+structure Object = struct type T = exn end;
+
 end;
 
 structure BasicLibrary: BASIC_LIBRARY = Library;