# HG changeset patch
# User wenzelm
# Date 1718016289 -7200
# Node ID 53f12ab896e6b63a626f7aeae7f71b9de412d227
# Parent  dca37c6479e3462d09980cbf0b2ec949a9b1f46f
clarified operations, following pretty_thm_name;

diff -r dca37c6479e3 -r 53f12ab896e6 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Jun 10 12:07:54 2024 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon Jun 10 12:44:49 2024 +0200
@@ -442,8 +442,7 @@
 
 fun pretty_term_abbrev ctxt = Syntax.pretty_term (set_mode mode_abbrev ctxt);
 
-fun pretty_fact_name ctxt a =
-  Pretty.block [Pretty.marks_str (markup_extern_fact ctxt a), Pretty.str ":"];
+fun pretty_fact_name ctxt a = Pretty.marks_str (markup_extern_fact ctxt a);
 
 fun pretty_fact ctxt =
   let
@@ -452,8 +451,10 @@
   in
     fn ("", [th]) => pretty_thm th
      | ("", ths) => Pretty.blk (0, Pretty.fbreaks (pretty_thms ths))
-     | (a, [th]) => Pretty.block [pretty_fact_name ctxt a, Pretty.brk 1, pretty_thm th]
-     | (a, ths) => Pretty.block (Pretty.fbreaks (pretty_fact_name ctxt a :: pretty_thms ths))
+     | (a, [th]) =>
+        Pretty.block [pretty_fact_name ctxt a, Pretty.str ":", Pretty.brk 1, pretty_thm th]
+     | (a, ths) =>
+        Pretty.block (Pretty.fbreaks (pretty_fact_name ctxt a :: Pretty.str ":" :: pretty_thms ths))
   end;