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;