--- 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;