diff -r 4898bae6ef23 -r 0a54cfc9add3 src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sat Nov 27 17:44:36 2010 -0800
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun Nov 28 15:20:51 2010 +0100
@@ -2929,7 +2929,7 @@
       using sf B(3)
       unfolding span_linear_image[OF lf] surj_def subset_eq image_iff
       apply blast
-      using fB apply (blast intro: finite_imageI)
+      using fB apply blast
       unfolding d[symmetric]
       apply (rule card_image_le)
       apply (rule fB)
@@ -3035,7 +3035,7 @@
   shows "finite {abs((x::'a::euclidean_space)$$i) |i. i<DIM('a)}"
   and "{abs(x$$i) |i. i<DIM('a::euclidean_space)} \<noteq> {}"
   unfolding infnorm_set_image
-  by (auto intro: finite_imageI)
+  by auto
 
 lemma infnorm_pos_le: "0 \<le> infnorm (x::'a::euclidean_space)"
   unfolding infnorm_def