| changeset 45136 | 2afb928c71ca |
| parent 44427 | c4a86d72a5cc |
| child 45666 | d83797ef0d2d |
--- a/src/Pure/Concurrent/future.ML Thu Oct 13 13:49:55 2011 +0200 +++ b/src/Pure/Concurrent/future.ML Thu Oct 13 22:50:35 2011 +0200 @@ -552,7 +552,7 @@ fun value_result (res: 'a Exn.result) = let - val task = Task_Queue.dummy_task (); + val task = Task_Queue.dummy_task; val group = Task_Queue.group_of_task task; val result = Single_Assignment.var "value" : 'a result; val _ = assign_result group result res;