diff -r 89038d9ef77d -r 909dc00766a0 src/Pure/Concurrent/event_timer.ML --- a/src/Pure/Concurrent/event_timer.ML Tue Sep 26 14:29:55 2023 +0200 +++ b/src/Pure/Concurrent/event_timer.ML Tue Sep 26 14:42:33 2023 +0200 @@ -134,7 +134,7 @@ manager_loop); fun shutdown () = - Thread_Attributes.uninterruptible (fn run => fn () => + Thread_Attributes.uninterruptible_body (fn run => if Synchronized.change_result state (fn st as State {requests, manager, ...} => if is_shutdown Normal st then (false, st) else if is_shutdown Shutdown_Ack st orelse is_shutdown_req st then @@ -149,7 +149,7 @@ Synchronized.change state (fn State {requests, manager, ...} => make_state (requests, Normal, manager)) else () - else ()) (); + else ()); (* main operations *) @@ -170,12 +170,12 @@ in (canceled, make_state (requests', status, manager')) end); fun future physical time = - Thread_Attributes.uninterruptible (fn _ => fn () => + Thread_Attributes.uninterruptible_body (fn _ => let val req: request Single_Assignment.var = Single_Assignment.var "req"; fun abort () = ignore (cancel (Single_Assignment.await req)); val promise: unit future = Future.promise_name "event_timer" abort; val _ = Single_Assignment.assign req (request physical time (Future.fulfill promise)); - in promise end) (); + in promise end); end;