--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Sat May 25 15:37:53 2013 +0200
@@ -28,18 +28,19 @@
syntax "_finite_vec" :: "type \<Rightarrow> type \<Rightarrow> type" ("(_ ^/ _)" [15, 16] 15)
parse_translation {*
-let
- fun vec t u = Syntax.const @{type_syntax vec} $ t $ u;
- fun finite_vec_tr [t, u] =
- (case Term_Position.strip_positions u of
- v as Free (x, _) =>
- if Lexicon.is_tid x then
- vec t (Syntax.const @{syntax_const "_ofsort"} $ v $ Syntax.const @{class_syntax finite})
- else vec t u
- | _ => vec t u)
-in
- [(@{syntax_const "_finite_vec"}, finite_vec_tr)]
-end
+ let
+ fun vec t u = Syntax.const @{type_syntax vec} $ t $ u;
+ fun finite_vec_tr [t, u] =
+ (case Term_Position.strip_positions u of
+ v as Free (x, _) =>
+ if Lexicon.is_tid x then
+ vec t (Syntax.const @{syntax_const "_ofsort"} $ v $
+ Syntax.const @{class_syntax finite})
+ else vec t u
+ | _ => vec t u)
+ in
+ [(@{syntax_const "_finite_vec"}, K finite_vec_tr)]
+ end
*}
lemma vec_eq_iff: "(x = y) \<longleftrightarrow> (\<forall>i. x$i = y$i)"