--- a/src/HOL/Analysis/Lebesgue_Measure.thy Sun Dec 30 10:34:56 2018 +0000
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy Sun Dec 30 10:34:56 2018 +0000
@@ -407,7 +407,7 @@
lemma measurable_lebesgue_cong:
assumes "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
shows "f \<in> measurable (lebesgue_on S) M \<longleftrightarrow> g \<in> measurable (lebesgue_on S) M"
- by (metis (mono_tags, lifting) IntD1 assms measurable_cong_strong space_restrict_space)
+ by (metis (mono_tags, lifting) IntD1 assms measurable_cong_simp space_restrict_space)
text%unimportant \<open>Measurability of continuous functions\<close>