author | wenzelm |
Tue, 11 Apr 2023 09:54:46 +0200 | |
changeset 77815 | c3330a54b9e5 |
parent 77814 | 53c5ad1a7ac0 |
child 77816 | aa814dc5a685 |
--- a/src/Pure/General/name_space.ML Tue Apr 11 09:49:30 2023 +0200 +++ b/src/Pure/General/name_space.ML Tue Apr 11 09:54:46 2023 +0200 @@ -113,7 +113,7 @@ pos: Position.T, serial: serial}; -fun entry_markup def kind (name, {pos, theory_long_name, serial, ...}: entry) = +fun entry_markup def kind (name, {pos, serial, ...}: entry) = Position.make_entity_markup def serial kind (name, pos); fun print_entry_ref kind (name, entry) =