tuned signature;
authorwenzelm
Fri, 27 Sep 2024 22:28:46 +0200
changeset 80980 54f5d6e1c317
parent 80979 e38c65002f44
child 80981 a594b5e922ad
tuned signature;
src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Fri Sep 27 22:14:40 2024 +0200
+++ b/src/Pure/Syntax/parser.ML	Fri Sep 27 22:28:46 2024 +0200
@@ -614,14 +614,14 @@
                 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*)
+                    SOME (used_prec, used_trees) => (*nonterminal has been processed*)
                       if used_prec <= min_prec then
                         (*wanted precedence has been processed*)
-                        (used, Parsetrees.fold movedot_lambda l States)
+                        (used, Parsetrees.fold movedot_lambda used_trees States)
                       else (*wanted precedence hasn't been parsed yet*)
                         let
                           val States' = States |> add_prods i c nt (until_prec min_prec used_prec)
-                            |> Parsetrees.fold movedot_lambda l;
+                            |> Parsetrees.fold movedot_lambda used_trees;
                         in (update_prec (nt, min_prec) used, States') end
                   | NONE => (*nonterminal is parsed for the first time*)
                       let val States' = States |> add_prods i c nt (until_prec min_prec no_prec);