src/Pure/System/scala.ML

--- a/src/Pure/System/scala.ML	Thu Sep 28 11:30:01 2023 +0200
+++ b/src/Pure/System/scala.ML	Thu Sep 28 14:43:07 2023 +0200
@@ -60,8 +60,9 @@
             | NONE => SOME (Isabelle_Thread.interrupt_exn, tab)));
     in
       invoke ();
-      Exn.release (run await_result ())
-        handle exn => (if Exn.is_interrupt exn then cancel () else (); Exn.reraise exn)
+      (case Exn.capture (fn () => Exn.release (run await_result ())) () of
+        Exn.Res res => res
+      | Exn.Exn exn => (if Exn.is_interrupt exn then cancel () else (); Exn.reraise exn))
     end);
 
 val function1_bytes = singleton o function_bytes;