--- a/src/HOL/Algebra/Polynomials.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Algebra/Polynomials.thy Wed Oct 09 23:38:29 2024 +0200
@@ -1359,7 +1359,8 @@
subsection \<open>Algebraic Structure of Polynomials\<close>
-definition univ_poly :: "('a, 'b) ring_scheme \<Rightarrow>'a set \<Rightarrow> ('a list) ring" (\<open>_ [X]\<index>\<close> 80)
+definition univ_poly :: "('a, 'b) ring_scheme \<Rightarrow>'a set \<Rightarrow> ('a list) ring"
+ (\<open>(\<open>open_block notation=\<open>postfix X\<close>\<close>_ [X]\<index>)\<close> 80)
where "univ_poly R K =
\<lparr> carrier = { p. polynomial\<^bsub>R\<^esub> K p },
mult = ring.poly_mult R,