src/Pure/theory.ML
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