--- a/src/HOL/Library/Infinite_Set.thy Sat Nov 27 17:44:36 2010 -0800
+++ b/src/HOL/Library/Infinite_Set.thy Sun Nov 28 15:20:51 2010 +0100
@@ -339,7 +339,7 @@
shows "\<exists>y \<in> f`A. infinite (f -` {y})"
proof (rule ccontr)
assume "\<not> ?thesis"
- with img have "finite (UN y:f`A. f -` {y})" by (blast intro: finite_UN_I)
+ with img have "finite (UN y:f`A. f -` {y})" by blast
moreover have "A \<subseteq> (UN y:f`A. f -` {y})" by auto
moreover note dom
ultimately show False by (simp add: infinite_super)