diff -r 7b3b27576f45 -r 0fb1e2dd4122 src/HOL/Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Fri Oct 04 23:38:04 2024 +0200
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Sat Oct 05 14:58:36 2024 +0200
@@ -25,11 +25,6 @@
 notation vec_nth (infixl \<open>$\<close> 90) and vec_lambda (binder \<open>\<chi>\<close> 10)
 end
 
-bundle no_vec_syntax
-begin
-no_notation vec_nth (infixl \<open>$\<close> 90) and vec_lambda (binder \<open>\<chi>\<close> 10)
-end
-
 text \<open>
   Concrete syntax for \<open>('a, 'b) vec\<close>:
     \<^item> \<open>'a^'b\<close> becomes \<open>('a, 'b::finite) vec\<close>