diff -r 52d0b5fcb19d -r f1380c9f3806 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Wed Nov 25 13:51:28 2020 +0100
+++ b/src/Pure/PIDE/markup.ML	Wed Nov 25 15:12:02 2020 +0100
@@ -59,7 +59,6 @@
   val end_offsetN: string
   val fileN: string
   val idN: string
-  val position_properties': string list
   val position_properties: string list
   val positionN: string val position: T
   val expressionN: string val expression: string -> T
@@ -380,8 +379,7 @@
 val fileN = "file";
 val idN = "id";
 
-val position_properties' = [fileN, idN];
-val position_properties = [lineN, offsetN, end_offsetN] @ position_properties';
+val position_properties = [lineN, offsetN, end_offsetN, fileN, idN];
 
 val (positionN, position) = markup_elem "position";