--- 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 =