minor performance tuning;
authorwenzelm
Sat, 28 Sep 2024 16:11:30 +0200
changeset 80987 e7a926b5b5be
parent 80986 6e3e1e4a804d
child 80988 f1991616c5c3
minor performance tuning;
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*)