added structure Object (from Pure/General/object.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;