| changeset 77815 | c3330a54b9e5 |
| parent 75983 | 34dd96a06c45 |
| child 77819 | d2645d3ad9e9 |
--- 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) =