actually ensure globally unique counter results (amending a5853334c179);

--- 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;