diff -r 348aed032cda -r 36ffe23b25f8 src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
--- 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)"