# HG changeset patch
# User wenzelm
# Date 1734210279 -3600
# Node ID 775dc5903ed5091418f1973080f86c5de513334a
# Parent  d570d215e38009c00ee99d32f1567d8d6ec0e7a8
tuned signature: avoid shadowing;

diff -r d570d215e380 -r 775dc5903ed5 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Sat Dec 14 21:47:20 2024 +0100
+++ b/src/Pure/Syntax/syntax.ML	Sat Dec 14 22:04:39 2024 +0100
@@ -537,7 +537,7 @@
   then filter (Graph.is_minimal consts) (Graph.all_preds consts [c])
   else [c];
 
-fun update_consts (c, bs) consts =
+fun add_consts (c, bs) consts =
   if c = "" orelse (null bs andalso (Lexicon.is_marked c orelse Graph.defined consts c))
   then consts
   else
@@ -581,7 +581,7 @@
     ({input = new_xprods @ input,
       keywords = (fold o Syntax_Ext.fold_delims) add_keywords new_xprods keywords,
       gram = if null new_xprods then gram else extend_gram new_xprods input gram,
-      consts = fold update_consts consts2 consts1,
+      consts = fold add_consts consts2 consts1,
       prmodes = insert (op =) mode prmodes,
       parse_ast_trtab =
         update_trtab "parse ast translation" (if_inout parse_ast_translation) parse_ast_trtab,