changeset 62920 | a5853334c179 |
parent 52537 | 4b5941730bd8 |
child 68804 | cbde6e3b132b |
--- a/src/Pure/Concurrent/counter.ML Sat Apr 09 11:34:23 2016 +0200 +++ b/src/Pure/Concurrent/counter.ML Sat Apr 09 11:35:01 2016 +0200 @@ -16,13 +16,12 @@ fun make () = let - val counter = Synchronized.var "counter" (0: int); + val counter = Synchronized.var "counter" 0; fun next () = Synchronized.change_result counter (fn i => - let val j = i + (1: int) + let val j = i + (if Thread_Data.is_virtual then 3 else 2) in (j, j) end); in next end; end; -