src/Pure/Tools/rail.ML
changeset 58978 e42da880c61e
parent 58928 23d0ffd48006
child 59058 a78612c67ec0
--- a/src/Pure/Tools/rail.ML	Tue Nov 11 15:55:31 2014 +0100
+++ b/src/Pure/Tools/rail.ML	Tue Nov 11 18:16:25 2014 +0100
@@ -283,7 +283,7 @@
 
 fun read ctxt (source: Symbol_Pos.source) =
   let
-    val {text, pos, ...} = source;
+    val {text, range = (pos, _), ...} = source;
     val _ = Context_Position.report ctxt pos Markup.language_rail;
     val toks = tokenize (Symbol_Pos.explode (text, pos));
     val _ = Context_Position.reports ctxt (maps reports_of_token toks);