src/HOL/Probability/Sigma_Algebra.thy

     fix x i assume "x \<in> ?A' i" thus "x \<in> ?r"
       by (auto intro!: exI[of _ "from_nat i"])
   qed
   have **: "range ?A' = range A"
     using surj_from_nat
-    by (auto simp: image_compose intro!: imageI)
+    by (auto simp: image_comp [symmetric] intro!: imageI)
   show ?thesis unfolding * ** ..
 qed
 
 lemma (in sigma_algebra) countable_Union [intro]:
   assumes "countable X" "X \<subseteq> M" shows "Union X \<in> M"

   shows "(g o f) \<in> measurable a c"
 proof -
   have fab: "f \<in> (space a -> space b)"
    and ba: "\<And>y. y \<in> sets b \<Longrightarrow> (f -` y) \<inter> (space a) \<in> sets a" using f
      by (auto simp add: measurable_def)
-  have eq: "\<And>y. f -` g -` y \<inter> space a = f -` (g -` y \<inter> t) \<inter> space a" using t
+  have eq: "\<And>y. (g \<circ> f) -` y \<inter> space a = f -` (g -` y \<inter> t) \<inter> space a" using t
     by force
   show ?thesis
-    apply (auto simp add: measurable_def vimage_compose)
+    apply (auto simp add: measurable_def vimage_comp)
     apply (metis funcset_mem fab g)
-    apply (subst eq, metis ba cb)
+    apply (subst eq)
+    apply (metis ba cb)
     done
 qed
 
 lemma measurable_mono1:
   "M' \<subseteq> Pow \<Omega> \<Longrightarrow> M \<subseteq> M' \<Longrightarrow>