# HG changeset patch # User wenzelm # Date 1460194501 -7200 # Node ID a5853334c17984b28e7aaf1096b3357f03992426 # Parent 9eb0359d6a77f9600ee3fadce701e838c27f74de ensure globally unique counter results; diff -r 9eb0359d6a77 -r a5853334c179 src/Pure/Concurrent/counter.ML --- 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; -