# HG changeset patch
# User wenzelm
# Date 1517070426 -3600
# Node ID 656720e8f44369e28c0b51bcb68a5cfdf313c075
# Parent  fb87a0e9af21bb5849b3988d4f511c1f062a616e
tuned;

diff -r fb87a0e9af21 -r 656720e8f443 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Sat Jan 27 17:23:21 2018 +0100
+++ b/src/Pure/Syntax/parser.ML	Sat Jan 27 17:27:06 2018 +0100
@@ -61,6 +61,9 @@
   known yet are associated with this token*)
 val unknown_start = Lexicon.eof;
 
+fun get_start (tok :: _) = tok
+  | get_start [] = unknown_start;
+
 (*get all NTs that are connected with a list of NTs*)
 fun connected_with _ ([]: nt_tag list) relatives = relatives
   | connected_with chains (root :: roots) relatives =
@@ -199,9 +202,7 @@
 
                             (*existing productions whose lookahead may depend on l*)
                             val tk_prods =
-                              these
-                                (AList.lookup (op =) nt_prods
-                                  (SOME (hd l_starts handle List.Empty => unknown_start)));
+                              these (AList.lookup (op =) nt_prods (SOME (get_start l_starts)));
 
                             (*add_lambda is true if an existing production of the nt
                               produces lambda due to the new lambda NT l*)