changeset 74183 | af81e4a307be |
parent 74112 | d0527bb2e590 |
child 74230 | d637611b41bd |
--- a/src/Pure/theory.ML Tue Aug 24 13:39:37 2021 +0200 +++ b/src/Pure/theory.ML Tue Aug 24 14:56:55 2021 +0200 @@ -120,9 +120,7 @@ fun theory_markup def name id pos = if id = 0 then Markup.empty - else - Markup.properties (Position.entity_properties_of def id pos) - (Markup.entity Markup.theoryN name); + else Position.make_entity_markup def id Markup.theoryN (name, pos); fun init_markup (name, pos) thy = let