# HG changeset patch
# User wenzelm
# Date 1727455618 -7200
# Node ID 0326af18b7a7723188e158131002cd5247877699
# Parent  7c1e735409907200c15b5b795cbb9231b70541c9
tuned;

diff -r 7c1e73540990 -r 0326af18b7a7 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Fri Sep 27 16:52:43 2024 +0200
+++ b/src/Pure/Syntax/parser.ML	Fri Sep 27 18:46:58 2024 +0200
@@ -614,23 +614,26 @@
             Markup (_, body) :: sa => process used ((info, body @ sa, ts) :: States) (Si, Sii)
           | Nonterminal (nt, min_prec) :: sa =>
               let (*predictor operation*)
-                fun mk_state (rhs, id, prod_prec) = ((nt, prod_prec, id, i), rhs, []);
-                fun movedot_lambda (t, k) = if min_prec <= k then SOME (info, sa, t @ ts) else NONE;
-                val (used', new_states) =
+                fun add_state (rhs, id, prod_prec) = cons ((nt, prod_prec, id, i), rhs, []);
+                fun movedot_lambda (t, k) = min_prec <= k ? cons (info, sa, t @ ts)
+                val (used', States') =
                   (case Inttab.lookup used nt of
                     SOME (used_prec, l) => (*nonterminal has been processed*)
                       if used_prec <= min_prec then
                         (*wanted precedence has been processed*)
-                        (used, map_filter movedot_lambda l)
+                        (used, fold_rev movedot_lambda l States)
                       else (*wanted precedence hasn't been parsed yet*)
                         let
-                          val States2 = map mk_state (prods_for c nt (until_prec min_prec used_prec));
-                          val States1 = map_filter movedot_lambda l;
-                        in (update_prec (nt, min_prec) used, States1 @ States2) end
+                          val States' = States
+                            |> fold_rev add_state (prods_for c nt (until_prec min_prec used_prec))
+                            |> fold_rev movedot_lambda l;
+                        in (update_prec (nt, min_prec) used, States') end
                   | NONE => (*nonterminal is parsed for the first time*)
-                      let val States' = map mk_state (prods_for c nt (until_prec min_prec no_prec))
+                      let
+                        val States' = States
+                          |> fold_rev add_state (prods_for c nt (until_prec min_prec no_prec));
                       in (Inttab.update (nt, (min_prec, [])) used, States') end);
-              in process used' (new_states @ States) (S :: Si, Sii) end
+              in process used' States' (S :: Si, Sii) end
           | Terminal a :: sa => (*scanner operation*)
               let
                 val (_, _, id, _) = info;