src/HOL/Analysis/Finite_Cartesian_Product.thy

 typedef ('a, 'b) vec = "UNIV :: ('b::finite \<Rightarrow> 'a) set"
   morphisms vec_nth vec_lambda ..
 
 declare vec_lambda_inject [simplified, simp]
 
-bundle vec_syntax begin
-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)
+bundle vec_syntax
+begin
+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
 
 unbundle vec_syntax
 
 text \<open>