diff -r c4fa2b381591 -r 063d2f23cdf6 src/Pure/Syntax/syntax_ext.ML
--- a/src/Pure/Syntax/syntax_ext.ML	Fri Apr 01 17:13:40 2016 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML	Fri Apr 01 17:14:27 2016 +0200
@@ -250,8 +250,7 @@
   Scan.repeat1 scan_delim_char >> (Delim o Symbol_Pos.content);
 
 val scan_symb =
-  Scan.trace scan_sym >>
-    (fn (syms, trace) => SOME (syms, Position.set_range (Symbol_Pos.range trace))) ||
+  Scan.trace scan_sym >> (fn (syms, trace) => SOME (syms, #1 (Symbol_Pos.range trace))) ||
   $$ "'" -- scan_one Symbol.is_blank >> K NONE;
 
 val scan_symbs = Scan.repeat scan_symb --| Scan.ahead (~$$ "'");