# HG changeset patch
# User wenzelm
# Date 1729544294 -7200
# Node ID f63ffe7f4234e5279c4fc574234f4275af25501a
# Parent  b61abd1e502754f12799f5ea0e53001676bba7f2
minor performance tuning;

diff -r b61abd1e5027 -r f63ffe7f4234 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Mon Oct 21 22:28:07 2024 +0200
+++ b/src/Pure/Syntax/parser.ML	Mon Oct 21 22:58:14 2024 +0200
@@ -661,11 +661,11 @@
 fun update_prec (A, p) used =
   Inttab.map_default (A, init_prec) (fn (_, output) => (p, output)) used;
 
-fun movedot_states out' A min max = map_filter
+fun movedot_states out' A min max = build o fold
   (fn ((info, Nonterminal (B, p) :: sa, out): state) =>
-      if A = B andalso upto_prec min max p then SOME (info, sa, append_output out' out)
-      else NONE
-    | _ => NONE);
+      if A = B andalso upto_prec min max p then cons (info, sa, append_output out' out)
+      else I
+    | _ => I);
 
 fun process_states (Gram {prods = gram_prods, chains = gram_chains, ...}) stateset i c states0 =
   let