# HG changeset patch
# User wenzelm
# Date 852566529 -3600
# Node ID 09634c9cbf3ce0fa867190f94c1e7aa8f927b083
# Parent  273580d5c04020b87cbf9179aabb1ab1a46d37c1
added stamp util;

diff -r 273580d5c040 -r 09634c9cbf3c src/Pure/library.ML
--- a/src/Pure/library.ML	Fri Jan 03 15:25:51 1997 +0100
+++ b/src/Pure/library.ML	Mon Jan 06 17:02:09 1997 +0100
@@ -45,6 +45,13 @@
 
 
 
+(** stamps **)
+
+type stamp = unit ref;
+val stamp: unit -> stamp = ref;
+
+
+
 (** options **)
 
 datatype 'a option = None | Some of 'a;