changeset 67551 | 4a087b9a29c5 |
parent 67550 | 3b666615e3ce |
child 67552 | 679253fef277 |
--- a/src/Pure/Syntax/parser.ML Wed Jan 31 11:23:53 2018 +0100 +++ b/src/Pure/Syntax/parser.ML Wed Jan 31 11:26:50 2018 +0100 @@ -710,7 +710,7 @@ val end_pos = (case try List.last toks of NONE => Position.none - | SOME (Lexicon.Token (_, _, (_, end_pos))) => end_pos); + | SOME tok => Lexicon.end_pos_of_token tok); val r = (case earley gram start (toks @ [Lexicon.mk_eof end_pos]) of [] => raise Fail "Inner syntax: no parse trees"