diff -r d64d48eb71cc -r 4af607652318 src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Tue Feb 10 16:09:30 2015 +0000
+++ b/src/HOL/Library/Infinite_Set.thy	Tue Feb 10 17:37:06 2015 +0000
@@ -238,7 +238,7 @@
   from inf have "infinite {x. P x}" unfolding Inf_many_def .
   moreover from q have "{x. P x} \<subseteq> {x. Q x}" by auto
   ultimately show ?thesis
-    by (simp add: Inf_many_def infinite_super)
+    using Inf_many_def infinite_super by blast
 qed
 
 lemma MOST_mono: "\<forall>\<^sub>\<infinity>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> \<forall>\<^sub>\<infinity>x. Q x"