diff -r 3457d7d43ee9 -r bc7a6455e12a src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Tue Dec 12 13:34:11 2017 +0100
+++ b/src/Pure/PIDE/markup.ML	Tue Dec 12 16:12:48 2017 +0100
@@ -54,7 +54,6 @@
   val position_properties': string list
   val position_properties: string list
   val positionN: string val position: T
-  val rangeN: string
   val expressionN: string val expression: string -> T
   val citationN: string val citation: string -> T
   val pathN: string val path: string -> T
@@ -337,8 +336,6 @@
 
 val (positionN, position) = markup_elem "position";
 
-val rangeN = "range";
-
 
 (* expression *)