| changeset 43727 | a0c3de0573d4 |
| parent 40449 | 9c390868d255 |
| child 43761 | e72ba84ae58f |
--- a/src/Pure/Concurrent/synchronized.ML Sun Jul 10 16:09:08 2011 +0200 +++ b/src/Pure/Concurrent/synchronized.ML Sun Jul 10 16:13:37 2011 +0200 @@ -71,11 +71,11 @@ fun counter () = let - val counter = var "counter" 0; + val counter = var "counter" (0: int); fun next () = change_result counter (fn i => - let val j = i + 1 + let val j = i + (1: int) in (j, j) end); in next end;