diff -r f4c07fdd1d48 -r 4a8431c73cf2 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Sun Jan 09 13:58:31 2011 +0100
+++ b/src/Pure/General/markup.ML	Sun Jan 09 16:03:56 2011 +0100
@@ -22,8 +22,6 @@
   val lineN: string
   val columnN: string
   val offsetN: string
-  val end_lineN: string
-  val end_columnN: string
   val end_offsetN: string
   val fileN: string
   val idN: string
@@ -187,13 +185,11 @@
 val lineN = "line";
 val columnN = "column";
 val offsetN = "offset";
-val end_lineN = "end_line";
-val end_columnN = "end_column";
 val end_offsetN = "end_offset";
 val fileN = "file";
 val idN = "id";
 
-val position_properties' = [end_lineN, end_columnN, end_offsetN, fileN, idN];
+val position_properties' = [end_offsetN, fileN, idN];
 val position_properties = [lineN, columnN, offsetN] @ position_properties';
 
 val (positionN, position) = markup_elem "position";