diff -r 2d0cf40f6fb3 -r 06e195515deb src/HOL/Probability/Caratheodory.thy
--- a/src/HOL/Probability/Caratheodory.thy	Tue Jul 01 11:06:31 2014 +0200
+++ b/src/HOL/Probability/Caratheodory.thy	Mon Jun 30 15:45:03 2014 +0200
@@ -640,8 +640,7 @@
 
 lemma measure_down:
   "measure_space \<Omega> N \<mu> \<Longrightarrow> sigma_algebra \<Omega> M \<Longrightarrow> M \<subseteq> N \<Longrightarrow> measure_space \<Omega> M \<mu>"
-  by (simp add: measure_space_def positive_def countably_additive_def)
-     blast
+  by (auto simp add: measure_space_def positive_def countably_additive_def subset_eq)
 
 subsection {* Caratheodory's theorem *}