# HG changeset patch
# User wenzelm
# Date 1517319093 -3600
# Node ID ca8fec4a00fa7bc80e5c1bbae798bcbb29ebeb3f
# Parent  f253e5eaf995cd7e021faa0be96f6ccd60f0380e
tuned;

diff -r f253e5eaf995 -r ca8fec4a00fa src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Tue Jan 30 14:27:14 2018 +0100
+++ b/src/Pure/Syntax/parser.ML	Tue Jan 30 14:31:33 2018 +0100
@@ -180,7 +180,7 @@
                                   is_none tk andalso forall (nts_member lambdas) nts;
 
                                 val new_tks =
-                                  (if is_some tk then [the tk] else [])
+                                  the_list tk
                                   |> fold (tokens_union o starts_for_nt) nts
                                   |> subtract (op =) l_starts;
 
@@ -265,7 +265,7 @@
               val (start_tk, start_nts) = lookahead_dependency lambdas' rhs [];
 
               val start_tks =
-                (if is_some start_tk then [the start_tk] else [])
+                the_list start_tk
                 |> fold (tokens_union o starts_for_nt) start_nts;
 
               val opt_starts =