# HG changeset patch
# User wenzelm
# Date 1737638731 -3600
# Node ID adda8961df7bb1ade02a6017cfc570629e7319a5
# Parent  658f3237eaddbb2f14474bdcae964fad89069a23
tuned output;

diff -r 658f3237eadd -r adda8961df7b src/Pure/Isar/runtime.ML
--- 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 =