diff -r 708d301205fe -r 53fcbede7bf7 src/Pure/Syntax/parser.ML --- a/src/Pure/Syntax/parser.ML Mon Feb 24 21:43:52 2020 +0100 +++ b/src/Pure/Syntax/parser.ML Mon Feb 24 22:14:52 2020 +0100 @@ -128,7 +128,12 @@ if chains_member chains (from, lhs) then (SOME from, false, chains) else (SOME from, true, chains_insert (from, lhs) chains) - | _ => (NONE, false, chains_declare lhs chains)); + | _ => + let + val chains' = chains + |> chains_declare lhs + |> fold (fn Nonterminal (nt, _) => chains_declare nt | _ => I) rhs; + in (NONE, false, chains') end); (*propagate new chain in lookahead and lambdas; added_starts is used later to associate existing