--- a/src/HOL/Computational_Algebra/Polynomial.thy Mon Sep 30 22:57:45 2024 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial.thy Mon Sep 30 23:32:26 2024 +0200
@@ -349,7 +349,7 @@
subsection \<open>List-style syntax for polynomials\<close>
syntax
- "_poly" :: "args \<Rightarrow> 'a poly" (\<open>[:(\<open>notation=\<open>mixfix polynomial enumeration\<close>\<close>_):]\<close>)
+ "_poly" :: "args \<Rightarrow> 'a poly" (\<open>(\<open>indent=2 notation=\<open>mixfix polynomial enumeration\<close>\<close>[:_:])\<close>)
syntax_consts
pCons
translations