diff -r 843dba3d307a -r c007e6d9941d src/HOL/Computational_Algebra/Polynomial.thy
--- a/src/HOL/Computational_Algebra/Polynomial.thy	Mon Sep 30 23:32:26 2024 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial.thy	Tue Oct 01 20:39:16 2024 +0200
@@ -350,8 +350,6 @@
 
 syntax
   "_poly" :: "args \<Rightarrow> 'a poly"  (\<open>(\<open>indent=2 notation=\<open>mixfix polynomial enumeration\<close>\<close>[:_:])\<close>)
-syntax_consts
-  pCons
 translations
   "[:x, xs:]" \<rightleftharpoons> "CONST pCons x [:xs:]"
   "[:x:]" \<rightleftharpoons> "CONST pCons x 0"