src/Pure/Concurrent/future.ML
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;