# HG changeset patch
# User wenzelm
# Date 1322165720 -3600
# Node ID b4f374a45668e6b6acea27f95d4c24bd259e8888
# Parent  750c5a47400bb835fbdfa80c8e246b50e1da099b
more abstract datatype stamp, which avoids pointless allocation of mutable cells;

diff -r 750c5a47400b -r b4f374a45668 src/Pure/library.ML
--- a/src/Pure/library.ML	Thu Nov 24 21:01:06 2011 +0100
+++ b/src/Pure/library.ML	Thu Nov 24 21:15:20 2011 +0100
@@ -212,11 +212,11 @@
   val partition_eq: ('a * 'a -> bool) -> 'a list -> 'a list list
   val partition_list: (int -> 'a -> bool) -> int -> int -> 'a list -> 'a list list
   val legacy_gensym: string -> string
-  type stamp = unit Unsynchronized.ref
-  val stamp: unit -> stamp
   type serial = int
   val serial: unit -> serial
   val serial_string: unit -> string
+  eqtype stamp
+  val stamp: unit -> stamp
   structure Object: sig type T = exn end
   val cd: string -> unit
   val pwd: unit -> string
@@ -1068,15 +1068,15 @@
 end;
 
 
-(* stamps and serial numbers *)
-
-type stamp = unit Unsynchronized.ref;
-val stamp: unit -> stamp = Unsynchronized.ref;
+(* serial numbers and abstract stamps *)
 
 type serial = int;
 val serial = Multithreading.serial;
 val serial_string = string_of_int o serial;
 
+datatype stamp = Stamp of serial;
+fun stamp () = Stamp (serial ());
+
 
 (* generic objects *)