# HG changeset patch
# User wenzelm
# Date 1727532690 -7200
# Node ID e7a926b5b5bef3486b0a250e0aa9b3114bf369b5
# Parent  6e3e1e4a804dc50b0e5d61c248c587efb41a99ee
minor performance tuning;

diff -r 6e3e1e4a804d -r e7a926b5b5be src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Sat Sep 28 16:07:46 2024 +0200
+++ b/src/Pure/Syntax/parser.ML	Sat Sep 28 16:11:30 2024 +0200
@@ -604,7 +604,7 @@
             Markup (_, body) :: sa => process used ((info, body @ sa, ts) :: states) (Si, Sii)
           | Nonterminal (nt, min_prec) :: sa =>
               let (*predictor operation*)
-                fun movedot_lambda (t, k) = min_prec <= k ? cons (info, sa, t @ ts)
+                fun movedot_lambda (t, k) = if min_prec <= k then cons (info, sa, t @ ts) else I;
                 val (used', states') =
                   (case Inttab.lookup used nt of
                     SOME (used_prec, used_trees) => (*nonterminal has been processed*)