diff -r 6458760261ca -r 34d1913f0b20 src/Pure/Tools/rail.ML
--- a/src/Pure/Tools/rail.ML	Sun Oct 18 18:09:48 2015 +0200
+++ b/src/Pure/Tools/rail.ML	Sun Oct 18 20:28:29 2015 +0200
@@ -85,8 +85,8 @@
 
 fun token k ss = [Token (Symbol_Pos.range ss, (k, Symbol_Pos.content ss))];
 
-fun antiq_token (antiq as (ss, {range, ...})) =
-  [Token (range, (Antiq antiq, Symbol_Pos.content ss))];
+fun antiq_token antiq =
+  [Token (#range antiq, (Antiq antiq, Symbol_Pos.content (#body antiq)))];
 
 val scan_space = Scan.many1 (Symbol.is_blank o Symbol_Pos.symbol);