diff -r 67d82d94a076 -r bfc0bb115fa1 src/Pure/Concurrent/counter.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/counter.scala	Mon Jul 04 20:18:19 2011 +0200
@@ -0,0 +1,27 @@
+/*  Title:      Pure/Concurrent/counter.scala
+    Author:     Makarius
+
+Synchronized counter for unique identifiers < 0.
+
+NB: ML ticks forwards, JVM ticks backwards.
+*/
+
+package isabelle
+
+
+object Counter
+{
+  type ID = Long
+}
+
+class Counter
+{
+  private var count: Counter.ID = 0
+
+  def apply(): Counter.ID = synchronized {
+    require(count > java.lang.Long.MIN_VALUE)
+    count -= 1
+    count
+  }
+}
+