Fixed nonterminating "blast" proof

--- a/src/HOL/Probability/Caratheodory.thy	Tue Oct 13 12:42:08 2015 +0100
+++ b/src/HOL/Probability/Caratheodory.thy	Tue Oct 13 14:49:15 2015 +0100
@@ -649,7 +649,7 @@
     with \<mu>'_spec[THEN bspec, of "\<Union>C"]
     obtain D where
       D: "D \<subseteq> M" "finite D" "disjoint D" "\<Union>C = \<Union>D" and "\<mu>' (\<Union>C) = (\<Sum>d\<in>D. \<mu> d)"
-      by blast
+      by auto
     with sum_eq[OF C D] have "\<mu>' (\<Union>C) = (\<Sum>c\<in>C. \<mu> c)" by simp }
   note \<mu>' = this