# HG changeset patch
# User wenzelm
# Date 1519831825 -3600
# Node ID 39d80006fc29a6ed6ec19a98660c4b67c51c6e3b
# Parent  184c293f0a33924623b4f2c88d0318fe72707ef4
more explicit infixl (see initial 1edf0f223c6e);
clarified name;

diff -r 184c293f0a33 -r 39d80006fc29 src/HOL/Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Wed Feb 28 13:37:33 2018 +0100
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Wed Feb 28 16:30:25 2018 +0100
@@ -39,7 +39,7 @@
     \<^item> \<open>'a^'b\<close> becomes \<open>('a, 'b::finite) vec\<close>
     \<^item> \<open>'a^'b::_\<close> becomes \<open>('a, 'b) vec\<close> without extra sort-constraint
 \<close>
-syntax "_finite_vec" :: "type \<Rightarrow> type \<Rightarrow> type" ("(_ ^/ _)" [15, 16] 15)
+syntax "_vec_type" :: "type \<Rightarrow> type \<Rightarrow> type" (infixl "^" 15)
 parse_translation \<open>
   let
     fun vec t u = Syntax.const @{type_syntax vec} $ t $ u;
@@ -52,7 +52,7 @@
           else vec t u
       | _ => vec t u)
   in
-    [(@{syntax_const "_finite_vec"}, K finite_vec_tr)]
+    [(@{syntax_const "_vec_type"}, K finite_vec_tr)]
   end
 \<close>