src/Pure/Tools/debugger.ML
changeset 78720 909dc00766a0
parent 78716 97dfba4405e3
child 78725 3c02ad5a1586
--- a/src/Pure/Tools/debugger.ML	Tue Sep 26 14:29:55 2023 +0200
+++ b/src/Pure/Tools/debugger.ML	Tue Sep 26 14:42:33 2023 +0200
@@ -229,13 +229,13 @@
 in
 
 fun debugger_loop thread_name =
-  Thread_Attributes.uninterruptible (fn run => fn () =>
+  Thread_Attributes.uninterruptible_body (fn run =>
     let
       fun loop () =
         (debugger_state thread_name; if debugger_command thread_name then loop () else ());
       val result = Exn.capture (run with_debugging) loop;
       val _ = debugger_state thread_name;
-    in Exn.release result end) ();
+    in Exn.release result end);
 
 end;