src/Pure/library.ML
changeset 16535 86c9eada525b
parent 16492 fbfd15412f05
child 16654 d964cbaa6c1c
     1.1 --- a/src/Pure/library.ML	Wed Jun 22 19:41:19 2005 +0200
     1.2 +++ b/src/Pure/library.ML	Wed Jun 22 19:41:20 2005 +0200
     1.3 @@ -263,6 +263,7 @@
     1.4    val stamp: unit -> stamp
     1.5    type serial
     1.6    val serial: unit -> serial
     1.7 +  structure Object: sig type T end
     1.8  end;
     1.9  
    1.10  signature LIBRARY =
    1.11 @@ -1299,6 +1300,13 @@
    1.12  local val count = ref 0
    1.13  in fun serial () = inc count end;
    1.14  
    1.15 +
    1.16 +(* generic objects *)
    1.17 +
    1.18 +(*note that the builtin exception datatype may be extended by new
    1.19 +  constructors at any time*)
    1.20 +structure Object = struct type T = exn end;
    1.21 +
    1.22  end;
    1.23  
    1.24  structure BasicLibrary: BASIC_LIBRARY = Library;