src/Pure/Tools/rail.ML
changeset 61473 34d1913f0b20
parent 61462 e16649b70107
child 61476 1884c40f1539
     1.1 --- a/src/Pure/Tools/rail.ML	Sun Oct 18 18:09:48 2015 +0200
     1.2 +++ b/src/Pure/Tools/rail.ML	Sun Oct 18 20:28:29 2015 +0200
     1.3 @@ -85,8 +85,8 @@
     1.4  
     1.5  fun token k ss = [Token (Symbol_Pos.range ss, (k, Symbol_Pos.content ss))];
     1.6  
     1.7 -fun antiq_token (antiq as (ss, {range, ...})) =
     1.8 -  [Token (range, (Antiq antiq, Symbol_Pos.content ss))];
     1.9 +fun antiq_token antiq =
    1.10 +  [Token (#range antiq, (Antiq antiq, Symbol_Pos.content (#body antiq)))];
    1.11  
    1.12  val scan_space = Scan.many1 (Symbol.is_blank o Symbol_Pos.symbol);
    1.13