diff -r 340df9f3491f -r 22f665a2e91c src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Probability/Borel_Space.thy	Mon Sep 12 07:55:43 2011 +0200
@@ -127,7 +127,7 @@
       "\<forall>S\<in>sets borel. ?f -` S \<inter> A \<in> op \<inter> A ` sets M"
     then have "?f -` S \<inter> A \<in> op \<inter> A ` sets M" by auto
     then have f: "?f -` S \<inter> A \<in> sets M"
-      using `A \<in> sets M` sets_into_space by fastsimp
+      using `A \<in> sets M` sets_into_space by fastforce
     show "?f -` S \<inter> space M \<in> sets M"
     proof cases
       assume "0 \<in> S"