diff -r 713424d012fd -r 70076ba563d2 src/HOL/Computational_Algebra/Polynomial.thy
--- a/src/HOL/Computational_Algebra/Polynomial.thy	Wed Aug 28 20:46:45 2024 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial.thy	Wed Aug 28 22:54:45 2024 +0200
@@ -348,7 +348,13 @@
 
 subsection \<open>List-style syntax for polynomials\<close>
 
-syntax "_poly" :: "args \<Rightarrow> 'a poly"  ("[:(_):]")
+nonterminal poly_args
+syntax
+  "" :: "'a \<Rightarrow> poly_args"  ("_")
+  "_poly_args" :: "'a \<Rightarrow> poly_args \<Rightarrow> poly_args"  ("_,/ _")
+  "_poly" :: "poly_args \<Rightarrow> 'a poly"  ("[:(_):]")
+syntax_consts
+  "_poly_args" "_poly" \<rightleftharpoons> pCons
 translations
   "[:x, xs:]" \<rightleftharpoons> "CONST pCons x [:xs:]"
   "[:x:]" \<rightleftharpoons> "CONST pCons x 0"