tuned output;

--- a/src/Pure/Isar/runtime.ML	Wed Jan 22 22:50:39 2025 +0100
+++ b/src/Pure/Isar/runtime.ML	Thu Jan 23 14:25:31 2025 +0100
@@ -106,6 +106,9 @@
         EXCURSION_FAIL (exn, loc) =>
           map (fn ((i, msg), id) => ((i, msg ^ Markup.markup Markup.no_report ("\n" ^ loc)), id))
             (sorted_msgs context exn)
+      | Morphism.MORPHISM (name, exn) =>
+          map (fn ((i, msg), id) => ((i, "MORPHISM " ^ quote name ^ "\n" ^ msg), id))
+            (sorted_msgs context exn)
       | _ =>
         let
           val msg =