diff -r 9576b510f6a2 -r e42da880c61e src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Tue Nov 11 15:55:31 2014 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Tue Nov 11 18:16:25 2014 +0100
@@ -462,10 +462,11 @@
       | decode ps (Ast.Appl asts) = decode_appl ps asts;
 
     val source = Syntax.read_token str;
+    val (pos, _) = #range source;
     val syms = Symbol_Pos.source_explode source;
     val ast =
-      parse_asts ctxt true root (syms, #pos source)
-      |> uncurry (report_result ctxt (#pos source))
+      parse_asts ctxt true root (syms, pos)
+      |> uncurry (report_result ctxt pos)
       |> decode [];
     val _ = Context_Position.reports_text ctxt (! reports);
   in ast end;