--- a/src/Pure/General/name_space.ML Tue Sep 07 21:47:50 2021 +0200
+++ b/src/Pure/General/name_space.ML Tue Sep 07 22:35:44 2021 +0200
@@ -113,8 +113,9 @@
pos: Position.T,
serial: serial};
-fun entry_markup def kind (name, {pos, serial, ...}: entry) =
- Position.make_entity_markup def serial kind (name, pos);
+fun entry_markup def kind (name, {pos, theory_long_name, serial, ...}: entry) =
+ Position.make_entity_markup def serial kind (name, pos)
+ ||> not (#def def) ? cons (Markup.def_theoryN, theory_long_name);
fun print_entry_ref kind (name, entry) =
quote (Markup.markup (entry_markup {def = false} kind (name, entry)) name);