src/HOL/Analysis/Measure_Space.thy

--- a/src/HOL/Analysis/Measure_Space.thy	Wed Apr 25 21:29:02 2018 +0100
+++ b/src/HOL/Analysis/Measure_Space.thy	Thu Apr 26 19:51:32 2018 +0200
@@ -1622,7 +1622,7 @@
     using emeasure_subadditive[OF measurable] fin
     apply simp
     apply (subst (asm) (2 3 4) emeasure_eq_ennreal_measure)
-    apply (auto simp add: ennreal_plus[symmetric] simp del: ennreal_plus)
+    apply (auto reorient: ennreal_plus)
     done
 qed