diff -r 1a829342a2d3 -r ce6e3bc34343 src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Wed May 10 19:30:17 2023 +0200
+++ b/src/Pure/ML/ml_compiler.ML	Wed May 10 20:30:46 2023 +0200
@@ -166,7 +166,8 @@
     (* input *)
 
     val position_props =
-      filter (fn (a, _) => a = Markup.idN orelse a = Markup.fileN) (Position.properties_of pos);
+      filter (fn (a, _) => a = Markup.labelN orelse a = Markup.fileN orelse a = Markup.idN)
+        (Position.properties_of pos);
     val location_props = op ^ (YXML.output_markup (":", position_props));
 
     val {explode_token, ...} = ML_Env.operations opt_context (#environment flags);