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