diff -r 079fe4292526 -r c7723cc15de8 src/HOL/Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Sun Aug 25 21:10:01 2024 +0200
@@ -40,6 +40,7 @@
     \<^item> \<open>'a^'b::_\<close> becomes \<open>('a, 'b) vec\<close> without extra sort-constraint
 \<close>
 syntax "_vec_type" :: "type \<Rightarrow> type \<Rightarrow> type" (infixl "^" 15)
+syntax_types "_vec_type" \<rightleftharpoons> vec
 parse_translation \<open>
   let
     fun vec t u = Syntax.const \<^type_syntax>\<open>vec\<close> $ t $ u;