# HG changeset patch
# User wenzelm
# Date 1146430206 -7200
# Node ID 94cd541dc8fa2110c249262eec62373e33c930e8
# Parent  b4bd790f93735b93a9a113dc238af3f81a84b95e
added serial_string;

diff -r b4bd790f9373 -r 94cd541dc8fa src/Pure/library.ML
--- a/src/Pure/library.ML	Sun Apr 30 22:50:05 2006 +0200
+++ b/src/Pure/library.ML	Sun Apr 30 22:50:06 2006 +0200
@@ -277,6 +277,7 @@
   val stamp: unit -> stamp
   type serial
   val serial: unit -> serial
+  val serial_string: unit -> string
   structure Object: sig type T end
 end;
 
@@ -1308,6 +1309,8 @@
 local val count = ref 0
 in fun serial () = inc count end;
 
+val serial_string = string_of_int o serial;
+
 
 (* generic objects *)