tuned;
authorwenzelm
Tue, 30 Jan 2018 14:31:33 +0100
changeset 67534 ca8fec4a00fa
parent 67533 f253e5eaf995
child 67535 99c08d541a7a
tuned;
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 =