--- 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>