diff -r 3a35ce87a55c -r 4b5941730bd8 src/Pure/Concurrent/synchronized.ML
--- a/src/Pure/Concurrent/synchronized.ML	Fri Jul 05 22:58:24 2013 +0200
+++ b/src/Pure/Concurrent/synchronized.ML	Fri Jul 05 23:10:18 2013 +0200
@@ -13,7 +13,6 @@
   val guarded_access: 'a var -> ('a -> ('b * 'a) option) -> 'b
   val change_result: 'a var -> ('a -> 'b * 'a) -> 'b
   val change: 'a var -> ('a -> 'a) -> unit
-  val counter: unit -> unit -> int
 end;
 
 structure Synchronized: SYNCHRONIZED =
@@ -66,18 +65,4 @@
 
 end;
 
-
-(* unique identifiers > 0 *)
-
-(*NB: ML ticks forwards, JVM ticks backwards*)
-fun counter () =
-  let
-    val counter = var "counter" (0: int);
-    fun next () =
-      change_result counter
-        (fn i =>
-          let val j = i + (1: int)
-          in (j, j) end);
-  in next end;
-
 end;