--- a/src/HOL/Analysis/Sigma_Algebra.thy Wed May 02 13:49:38 2018 +0200
+++ b/src/HOL/Analysis/Sigma_Algebra.thy Thu May 03 15:07:14 2018 +0200
@@ -2084,7 +2084,7 @@
have "(\<lambda>x. g (f x)) \<in> X \<rightarrow> space M" "\<And>A. A \<inter> f -` Y \<inter> X = A \<inter> X"
using * by auto
with * show "sets ?VV = sets ?V"
- by (simp add: sets_vimage_algebra2 ex_simps[symmetric] vimage_comp comp_def del: ex_simps)
+ by (simp add: sets_vimage_algebra2 vimage_comp comp_def reorient: ex_simps)
qed (simp add: vimage_algebra_def emeasure_sigma)
subsubsection \<open>Restricted Space Sigma Algebra\<close>