--- a/src/Pure/Isar/element.ML Sun Jun 09 15:11:07 2024 +0200
+++ b/src/Pure/Isar/element.ML Sun Jun 09 15:31:33 2024 +0200
@@ -228,7 +228,8 @@
let val head =
if Thm.has_name_hint th then
Pretty.block [Pretty.keyword1 kind, Pretty.brk 1,
- Proof_Context.pretty_name ctxt (Long_Name.base_name (Thm.get_name_hint th)), Pretty.str ":"]
+ Proof_Context.pretty_name ctxt (Long_Name.base_name (#1 (Thm.get_name_hint th))),
+ Pretty.str ":"]
else Pretty.keyword1 kind
in Pretty.block (Pretty.fbreaks (head :: prts)) end;