src/Pure/Tools/rail.ML
changeset 61476 1884c40f1539
parent 61473 34d1913f0b20
child 62748 aa0084adce1f
     1.1 --- a/src/Pure/Tools/rail.ML	Sun Oct 18 20:48:24 2015 +0200
     1.2 +++ b/src/Pure/Tools/rail.ML	Sun Oct 18 21:30:01 2015 +0200
     1.3 @@ -104,7 +104,7 @@
     1.4      [Token (Position.range pos1 pos2, (String, Symbol_Pos.content ss))]);
     1.5  
     1.6  val scan =
     1.7 -  (Scan.repeat scan_token >> flat) --|
     1.8 +  Scan.repeats scan_token --|
     1.9      Symbol_Pos.!!! (fn () => err_prefix ^ "bad input")
    1.10        (Scan.ahead (Scan.one Symbol_Pos.is_eof));
    1.11