diff -r 4898bae6ef23 -r 0a54cfc9add3 src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sat Nov 27 17:44:36 2010 -0800
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sun Nov 28 15:20:51 2010 +0100
@@ -1300,7 +1300,7 @@
   shows "finite {abs((x::'a::abs ^'n)$i) |i. i\<in> (UNIV :: 'n set)}"
   and "{abs(x$i) |i. i\<in> (UNIV :: 'n::finite set)} \<noteq> {}"
   unfolding  infnorm_set_image_cart
-  by (auto intro: finite_imageI)
+  by auto
 
 lemma component_le_infnorm_cart:
   shows "\<bar>x$i\<bar> \<le> infnorm (x::real^'n)"