src/Pure/Syntax/parser.ML
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"