src/Pure/Concurrent/lazy.ML

--- a/src/Pure/Concurrent/lazy.ML	Wed Oct 11 11:07:00 2023 +0200
+++ b/src/Pure/Concurrent/lazy.ML	Wed Oct 11 11:27:01 2023 +0200
@@ -101,8 +101,8 @@
               (case expr of
                 SOME (name, e) =>
                   let
-                    val res0 = Exn.capture (run e) ();
-                    val _ = Exn.capture (fn () => Future.fulfill_result x res0) ();
+                    val res0 = Exn.capture_body (run e);
+                    val _ = Exn.capture_body (fn () => Future.fulfill_result x res0);
                     val res = Future.get_result x;
                     val _ =
                       if not (Exn.is_interrupt_exn res) then
@@ -114,7 +114,7 @@
                         interrupt, until there is a fresh start*)
                       else Synchronized.change var (fn _ => Expr (name, e));
                   in res end
-              | NONE => Exn.capture (run (fn () => Future.join x)) ())
+              | NONE => Exn.capture_body (run (fn () => Future.join x)))
             end));
 
 end;