diff -r 817944aeac3f -r 2c58505bf151 src/HOL/Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Wed Feb 21 12:57:49 2018 +0000
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Thu Feb 22 18:01:08 2018 +0100
@@ -20,9 +20,19 @@
 
 declare vec_lambda_inject [simplified, simp]
 
+bundle vec_syntax begin
 notation
   vec_nth (infixl "$" 90) and
   vec_lambda (binder "\<chi>" 10)
+end
+
+bundle no_vec_syntax begin
+no_notation
+  vec_nth (infixl "$" 90) and
+  vec_lambda (binder "\<chi>" 10)
+end
+
+unbundle vec_syntax
 
 (*
   Translate "'b ^ 'n" into "'b ^ ('n :: finite)". When 'n has already more than