diff -r 3a35ce87a55c -r 4b5941730bd8 src/Pure/Concurrent/counter.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/counter.ML	Fri Jul 05 23:10:18 2013 +0200
@@ -0,0 +1,28 @@
+(*  Title:      Pure/Concurrent/counter.ML
+    Author:     Makarius
+
+Synchronized counter for unique identifiers > 0.
+
+NB: ML ticks forwards, JVM ticks backwards.
+*)
+
+signature COUNTER =
+sig
+  val make: unit -> unit -> int
+end;
+
+structure Counter: COUNTER =
+struct
+
+fun make () =
+  let
+    val counter = Synchronized.var "counter" (0: int);
+    fun next () =
+      Synchronized.change_result counter
+        (fn i =>
+          let val j = i + (1: int)
+          in (j, j) end);
+  in next end;
+
+end;
+