src/Pure/Syntax/parser.ML
changeset 71468 53fcbede7bf7
parent 69575 f77cc54f6d47
child 77723 b761c91c2447
--- 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