# HG changeset patch
# User wenzelm
# Date 1733912332 -3600
# Node ID cf4bebd770b5842bf6fa11364c058a4baed01638
# Parent  78b746a992114ca03f99b88f9a97fe7ee0c3b8cf
proper bundle binomial_syntax;
NB: precedence of "choose" changes silently from 65 to 64 in 200107cdd3ac, but old 65 was still seen in the wild;

diff -r 78b746a99211 -r cf4bebd770b5 NEWS
--- a/NEWS	Wed Dec 11 11:14:50 2024 +0100
+++ b/NEWS	Wed Dec 11 11:18:52 2024 +0100
@@ -106,6 +106,7 @@
   unbundle no abs_syntax
   unbundle no floor_ceiling_syntax
   unbundle no uminus_syntax
+  unbundle no binomial_syntax
   unbundle no funcset_syntax
 
 This is more robust than individual 'no_syntax' / 'no_notation'
diff -r 78b746a99211 -r cf4bebd770b5 src/HOL/Binomial.thy
--- a/src/HOL/Binomial.thy	Wed Dec 11 11:14:50 2024 +0100
+++ b/src/HOL/Binomial.thy	Wed Dec 11 11:18:52 2024 +0100
@@ -18,8 +18,13 @@
 
 text \<open>Combinatorial definition\<close>
 
-definition binomial :: "nat \<Rightarrow> nat \<Rightarrow> nat"  (infix \<open>choose\<close> 64)
-  where "n choose k = card {K\<in>Pow {0..<n}. card K = k}"
+definition binomial :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+  where "binomial n k = card {K\<in>Pow {0..<n}. card K = k}"
+
+open_bundle binomial_syntax
+begin
+notation binomial  (infix \<open>choose\<close> 64)
+end
 
 lemma binomial_right_mono:
   assumes "m \<le> n" shows "m choose k \<le> n choose k"
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