diff -r 21010d2b41e7 -r 58a0757031dd src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Thu May 20 23:22:37 2010 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Thu May 20 21:19:38 2010 -0700
@@ -75,8 +75,8 @@
   assumes a: "range a \<subseteq> sets M"
   shows "(\<Inter>i::nat. a i) \<in> sets M"
 proof -
-  have "space M - (\<Union>i. space M - a i) \<in> sets M" using a
-    by (blast intro: countable_UN compl_sets a) 
+  from a have "\<forall>i. a i \<in> sets M" by fast
+  hence "space M - (\<Union>i. space M - a i) \<in> sets M" by blast
   moreover
   have "(\<Inter>i. a i) = space M - (\<Union>i. space M - a i)" using space_closed a 
     by blast
@@ -161,7 +161,7 @@
 lemma sigma_sets_Un: 
   "a \<in> sigma_sets sp A \<Longrightarrow> b \<in> sigma_sets sp A \<Longrightarrow> a \<union> b \<in> sigma_sets sp A"
 apply (simp add: Un_range_binary range_binary_eq) 
-apply (metis Union COMBK_def binary_def fun_upd_apply) 
+apply (rule Union, simp add: binary_def COMBK_def fun_upd_apply)
 done
 
 lemma sigma_sets_Inter:
@@ -210,7 +210,7 @@
      "sigma_sets (space M) (sets M) = sets M"
 proof
   show "sets M \<subseteq> sigma_sets (space M) (sets M)"
-    by (metis Set.subsetI sigma_sets.Basic space_closed)
+    by (metis Set.subsetI sigma_sets.Basic)
   next
   show "sigma_sets (space M) (sets M) \<subseteq> sets M"
     by (metis sigma_sets_subset subset_refl)
@@ -221,7 +221,7 @@
   apply (auto simp add: sigma_algebra_def sigma_algebra_axioms_def
       algebra_def sigma_sets.Empty sigma_sets.Compl sigma_sets_Un) 
   apply (blast dest: sigma_sets_into_sp)
-  apply (blast intro: sigma_sets.intros) 
+  apply (rule sigma_sets.Union, fast)
   done
 
 lemma sigma_algebra_sigma: