# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1444744155 -3600
# Node ID 3c69ea85f8dd4667525d27efafd5680ccc20ab32
# Parent  d53db136e8fda950c9a359336639bd452bf45952
Fixed nonterminating "blast" proof

diff -r d53db136e8fd -r 3c69ea85f8dd src/HOL/Probability/Caratheodory.thy
--- 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