src/Pure/Concurrent/isabelle_thread.ML
changeset 78757 a094bf81a496
parent 78755 42e48ad59cda
child 78762 89202852e52c
--- a/src/Pure/Concurrent/isabelle_thread.ML	Wed Oct 11 11:07:00 2023 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.ML	Wed Oct 11 11:27:01 2023 +0200
@@ -148,6 +148,7 @@
 struct
   open Exn;
   val capture = capture0;
+  fun capture_body e = capture e ();
 end;
 
 fun expose_interrupt_result () =
@@ -156,7 +157,7 @@
     fun main () =
       (Thread_Attributes.set_attributes Thread_Attributes.test_interrupts;
        Thread.Thread.testInterrupt ());
-    val test = Exn.capture main ();
+    val test = Exn.capture_body main;
     val _ = Thread_Attributes.set_attributes orig_atts;
   in test end;
 
@@ -168,7 +169,7 @@
 
 fun try_finally e f =
   Thread_Attributes.uninterruptible_body (fn run =>
-    Exn.release (Exn.capture (run e) () before f ()));
+    Exn.release (Exn.capture_body (run e) before f ()));
 
 fun try e = Basics.try e ();
 fun can e = Basics.can e ();