diff -r 3a35ce87a55c -r 4b5941730bd8 src/Pure/Concurrent/event_timer.ML
--- a/src/Pure/Concurrent/event_timer.ML	Fri Jul 05 22:58:24 2013 +0200
+++ b/src/Pure/Concurrent/event_timer.ML	Fri Jul 05 23:10:18 2013 +0200
@@ -26,7 +26,7 @@
 
 (* type request *)
 
-val request_counter = Synchronized.counter ();
+val request_counter = Counter.make ();
 datatype request = Request of int;
 fun new_request () = Request (request_counter ());