src/HOL/Probability/Giry_Monad.thy

     fix A assume A: "A \<in> sets N"
     then have "(\<lambda>M'. emeasure (distr M' N f) A) \<in> borel_measurable (subprob_algebra M) \<longleftrightarrow>
       (\<lambda>M'. emeasure M' (f -` A \<inter> space M)) \<in> borel_measurable (subprob_algebra M)"
       by (intro measurable_cong)
          (auto simp: emeasure_distr space_subprob_algebra
-               intro!: arg_cong2[where f=emeasure] sets_eq_imp_space_eq arg_cong2[where f="op \<inter>"])
+               intro!: arg_cong2[where f=emeasure] sets_eq_imp_space_eq arg_cong2[where f="(\<inter>)"])
     also have "\<dots>"
       using A by (intro measurable_emeasure_subprob_algebra) simp
     finally show "(\<lambda>M'. emeasure (distr M' N f) A) \<in> borel_measurable (subprob_algebra M)" .
   qed (auto intro!: subprob_space.subprob_space_distr simp: space_subprob_algebra not_empty cong: measurable_cong_sets)
 qed (insert assms, auto simp: measurable_empty_iff space_subprob_algebra_empty_iff)