changeset 59180 | c0fa3b3bdabd |
parent 59054 | 61b723761dff |
child 59330 | cb3a4caf206d |
--- a/src/Pure/Concurrent/future.ML Mon Dec 22 19:47:58 2014 +0100 +++ b/src/Pure/Concurrent/future.ML Mon Dec 22 20:40:37 2014 +0100 @@ -522,8 +522,6 @@ let val _ = if forall is_finished xs then () - else if Multithreading.self_critical () then - raise Fail "Cannot join future values within critical section" else if is_some (worker_task ()) then join_work (map task_of xs) else List.app (ignore o Single_Assignment.await o result_of) xs; in map get_result xs end;