--- a/src/Pure/Isar/named_target.ML Wed Apr 19 23:27:55 2023 +0200
+++ b/src/Pure/Isar/named_target.ML Thu Apr 20 11:57:34 2023 +0200
@@ -97,7 +97,7 @@
theory_registration = Generic_Target.theory_registration,
locale_dependency = fn _ => error "Not possible in theory target",
pretty = fn ctxt => [Pretty.block [Pretty.keyword1 "theory", Pretty.brk 1,
- Pretty.str (Context.theory_name (Proof_Context.theory_of ctxt))]]}
+ Pretty.str (Context.theory_base_name (Proof_Context.theory_of ctxt))]]}
| operations (Locale locale) =
{define = Generic_Target.define (locale_foundation locale),
notes = Generic_Target.notes (Generic_Target.locale_target_notes locale),