# HG changeset patch
# User wenzelm
# Date 1748776363 -7200
# Node ID 33dba4986b9ff5a91268a56eab8e209934bddce0
# Parent  55260840696f4c025ccda4268fcaa98eb198104b
tuned;

diff -r 55260840696f -r 33dba4986b9f src/Pure/Build/build.ML
--- a/src/Pure/Build/build.ML	Sat May 31 11:29:10 2025 +0200
+++ b/src/Pure/Build/build.ML	Sun Jun 01 13:12:43 2025 +0200
@@ -83,13 +83,13 @@
             let
               val res =
                 theories |>
-                  (map (build_theories session_name)
+                  (maps (build_theories session_name)
                     |> session_timing
                     |> Exn.capture);
               val res1 =
                 (case res of
                   Exn.Res loaded_theories =>
-                    Exn.capture (apply_hooks session_name) (flat loaded_theories)
+                    Exn.capture (apply_hooks session_name) loaded_theories
                 | Exn.Exn exn => Exn.Exn exn);
               val res2 = Exn.capture_body Session.finish;