diff -r f14fcf94e0e9 -r 849efff7de15 src/HOL/Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Wed Oct 02 20:49:44 2024 +0200
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Wed Oct 02 22:08:52 2024 +0200
@@ -20,7 +20,7 @@
 
 declare vec_lambda_inject [simplified, simp]
 
-bundle vec_syntax
+open_bundle vec_syntax
 begin
 notation vec_nth (infixl \<open>$\<close> 90) and vec_lambda (binder \<open>\<chi>\<close> 10)
 end
@@ -30,8 +30,6 @@
 no_notation vec_nth (infixl \<open>$\<close> 90) and vec_lambda (binder \<open>\<chi>\<close> 10)
 end
 
-unbundle vec_syntax
-
 text \<open>
   Concrete syntax for \<open>('a, 'b) vec\<close>:
     \<^item> \<open>'a^'b\<close> becomes \<open>('a, 'b::finite) vec\<close>