diff -r c421ee0d2350 -r 24f2b57a34ea src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Wed Aug 06 00:10:08 2008 +0200
+++ b/src/Pure/General/position.ML	Wed Aug 06 00:10:13 2008 +0200
@@ -81,7 +81,7 @@
         NONE => NONE
       | SOME m => SOME (m, the_default 1 (get_int props Markup.columnN)));
     fun property name = the_list (find_first (fn (x: string, _) => x = name) props);
-  in (Pos (count, property Markup.fileN @ property Markup.idN)) end;
+  in Pos (count, maps property Markup.position_properties') end;
 
 fun properties_of (Pos (count, props)) =
   (case count of