--- a/src/Pure/Concurrent/future.ML Tue Sep 26 14:29:55 2023 +0200
+++ b/src/Pure/Concurrent/future.ML Tue Sep 26 14:42:33 2023 +0200
@@ -550,7 +550,7 @@
(* forked results: nested parallel evaluation *)
fun forked_results {name, deps} es =
- Thread_Attributes.uninterruptible (fn run => fn () =>
+ Thread_Attributes.uninterruptible_body (fn run =>
let
val (group, pri) =
(case worker_task () of
@@ -562,7 +562,7 @@
in
run join_results futures
handle exn => (if Exn.is_interrupt exn then cancel_group group else (); Exn.reraise exn)
- end) ();
+ end);
(* task context for running thread *)