# HG changeset patch
# User wenzelm
# Date 1727535484 -7200
# Node ID 8e123493e0ccbb8bdafd53f5f4f0c3a696ca0761
# Parent  f1991616c5c3daafc0e1a7de863a2144aab48bb9
tuned: more uniform;

diff -r f1991616c5c3 -r 8e123493e0cc src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Sat Sep 28 16:19:53 2024 +0200
+++ b/src/Pure/Syntax/parser.ML	Sat Sep 28 16:58:04 2024 +0200
@@ -573,8 +573,8 @@
     | SOME q => (q, if p > q then update (Parsetrees.update (t, p) ts) used else used))
   end;
 
-fun update_prec (A, p) used =
-  Inttab.map_entry A (fn (_, ts) => (p, ts)) used;
+val init_prec = (no_prec, Parsetrees.empty);
+fun update_prec (A, p) used = Inttab.map_default (A, init_prec) (fn (_, ts) => (p, ts)) used;
 
 fun get_states A min max =
   let
@@ -621,7 +621,7 @@
                         in (update_prec (nt, min_prec) used, states') end
                   | NONE => (*nonterminal is parsed for the first time*)
                       let val states' = states |> add_prods nt min_prec no_prec;
-                      in (Inttab.update (nt, (min_prec, Parsetrees.empty)) used, states') end);
+                      in (update_prec (nt, min_prec) used, states') end);
               in process used' states' (S :: Si, Sii) end
           | Terminal a :: sa => (*scanner operation*)
               let