src/Pure/Isar/outer_syntax.ML

--- a/src/Pure/Isar/outer_syntax.ML	Tue Aug 24 13:39:37 2021 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Aug 24 14:56:55 2021 +0200
@@ -65,8 +65,7 @@
 fun command_pos (Command {pos, ...}) = pos;
 
 fun command_markup def (name, Command {pos, id, ...}) =
-  Markup.properties (Position.entity_properties_of def id pos)
-    (Markup.entity Markup.commandN name);
+  Position.make_entity_markup def id Markup.commandN (name, pos);
 
 fun pretty_command (cmd as (name, Command {comment, ...})) =
   Pretty.block