| changeset 61473 | 34d1913f0b20 |
| parent 61462 | e16649b70107 |
| child 61476 | 1884c40f1539 |
--- 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);