--- a/src/Pure/Isar/element.ML Sun Jun 09 15:31:33 2024 +0200
+++ b/src/Pure/Isar/element.ML Sun Jun 09 19:49:42 2024 +0200
@@ -141,7 +141,7 @@
val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
val prt_terms = separate (Pretty.keyword2 "and") o map prt_term;
val prt_binding = Attrib.pretty_binding ctxt;
- val prt_name = Proof_Context.pretty_name ctxt;
+ val prt_name = Thy_Header.pretty_name' ctxt;
fun prt_show (a, ts) =
Pretty.block (Pretty.breaks (prt_binding a ":" @ prt_terms (map fst ts)));
@@ -167,7 +167,7 @@
val prt_typ = Pretty.quote o Syntax.pretty_typ ctxt;
val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
val prt_thm = Pretty.cartouche o Thm.pretty_thm ctxt;
- val prt_name = Proof_Context.pretty_name ctxt;
+ val prt_name = Thy_Header.pretty_name' ctxt;
fun prt_binding (b, atts) =
Attrib.pretty_binding ctxt (b, if show_attribs then atts else []);
@@ -228,7 +228,7 @@
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 (#1 (Thm.get_name_hint th))),
+ Thy_Header.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;