# HG changeset patch
# User wenzelm
# Date 1535186528 -7200
# Node ID cbde6e3b132b20a739ba94598896d40a59c2f5b9
# Parent  169bf32b35dd1a107f78bf97473d7b236a55b4c6
actually ensure globally unique counter results (amending a5853334c179);

diff -r 169bf32b35dd -r cbde6e3b132b src/Pure/Concurrent/counter.ML
--- a/src/Pure/Concurrent/counter.ML	Sat Aug 25 10:29:31 2018 +0200
+++ b/src/Pure/Concurrent/counter.ML	Sat Aug 25 10:42:08 2018 +0200
@@ -20,8 +20,10 @@
     fun next () =
       Synchronized.change_result counter
         (fn i =>
-          let val j = i + (if Thread_Data.is_virtual then 3 else 2)
-          in (j, j) end);
+          let
+            val k = i + 1;
+            val n = if Thread_Data.is_virtual then 2 * k + 1 else 2 * k;
+          in (n, k) end);
   in next end;
 
 end;