# HG changeset patch
# User wenzelm
# Date 1517394410 -3600
# Node ID 4a087b9a29c556c1fe6d6d08fbc09f3738676d31
# Parent  3b666615e3ce8032a3b63a81b92ab22ddda753f1
clarified signature;

diff -r 3b666615e3ce -r 4a087b9a29c5 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Wed Jan 31 11:23:53 2018 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Wed Jan 31 11:26:50 2018 +0100
@@ -28,6 +28,7 @@
   val kind_of_token: token -> token_kind
   val str_of_token: token -> string
   val pos_of_token: token -> Position.T
+  val end_pos_of_token: token -> Position.T
   val tokens_match_ord: token * token -> order
   val is_proper: token -> bool
   val dummy: token
@@ -146,6 +147,7 @@
 fun kind_of_token (Token (k, _, _)) = k;
 fun str_of_token (Token (_, s, _)) = s;
 fun pos_of_token (Token (_, _, (pos, _))) = pos;
+fun end_pos_of_token (Token (_, _, (_, end_pos))) = end_pos;
 
 fun tokens_match_ord toks =
   (case apply2 kind_of_token toks of
diff -r 3b666615e3ce -r 4a087b9a29c5 src/Pure/Syntax/parser.ML
--- 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"