| changeset 52537 | 4b5941730bd8 |
| parent 52050 | b40ed9dcf903 |
| child 52589 | d28d2d89034d |
--- 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 ());