src/Pure/ML/ml_compiler.ML

--- a/src/Pure/ML/ml_compiler.ML	Sat Apr 01 19:15:38 2023 +0200
+++ b/src/Pure/ML/ml_compiler.ML	Sat Apr 01 21:12:44 2023 +0200
@@ -165,7 +165,9 @@
 
     (* input *)
 
-    val location_props = op ^ (YXML.output_markup (":", #props (Position.dest pos)));
+    val position_props =
+      filter (fn (a, _) => a = Markup.idN orelse a = Markup.fileN) (Position.properties_of pos);
+    val location_props = op ^ (YXML.output_markup (":", position_props));
 
     val {explode_token, ...} = ML_Env.operations opt_context (#environment flags);
     fun token_content tok = if ML_Lex.is_comment tok then NONE else SOME (`explode_token tok);