diff -r 78b746a99211 -r cf4bebd770b5 src/HOL/HOLCF/Universal.thy
--- a/src/HOL/HOLCF/Universal.thy	Wed Dec 11 11:14:50 2024 +0100
+++ b/src/HOL/HOLCF/Universal.thy	Wed Dec 11 11:18:52 2024 +0100
@@ -8,7 +8,7 @@
 imports Bifinite Completion "HOL-Library.Nat_Bijection"
 begin
 
-no_notation binomial  (infix \<open>choose\<close> 64)
+unbundle no binomial_syntax
 
 
 subsection \<open>Basis for universal domain\<close>
@@ -983,6 +983,6 @@
 
 hide_const (open) node
 
-notation binomial  (infixl \<open>choose\<close> 65)
+unbundle binomial_syntax
 
 end