diff -r 374caac3d624 -r 125705f5965f src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sun Sep 15 17:24:31 2019 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Mon Sep 16 17:03:13 2019 +0100
@@ -4611,7 +4611,7 @@
   have "(UNIV::'a set) \<in> sets lborel"
     by simp
   then show ?thesis
-    using assms borel_measurable_if_D borel_measurable_UNIV_eq integrable_imp_measurable_weak integrable_restrict_UNIV by blast
+    by (metis (mono_tags, lifting) assms borel_measurable_if_D integrable_imp_measurable_weak integrable_restrict_UNIV lebesgue_on_UNIV_eq sets_lebesgue_on_refl)
 qed
 
 lemma integrable_iff_integrable_on:
@@ -4767,7 +4767,7 @@
     then have "(\<lambda>x. if x \<in> S then f x else 0) integrable_on UNIV"
       by (simp add: integrable_restrict_UNIV)
     then have borel: "(\<lambda>x. if x \<in> S then f x else 0) \<in> borel_measurable (lebesgue_on UNIV)"
-      using integrable_imp_measurable borel_measurable_UNIV_eq by blast
+      using integrable_imp_measurable lebesgue_on_UNIV_eq by blast
     then show "{x \<in> S. f x \<noteq> 0} \<in> sets lebesgue"
       unfolding borel_measurable_vimage_open
       by (rule allE [where x = "-{0}"]) auto
@@ -4777,7 +4777,7 @@
     then have "(\<lambda>x. if x \<in> T then f x else 0) integrable_on UNIV"
       by (simp add: integrable_restrict_UNIV)
     then have borel: "(\<lambda>x. if x \<in> T then f x else 0) \<in> borel_measurable (lebesgue_on UNIV)"
-      using integrable_imp_measurable borel_measurable_UNIV_eq by blast
+      using integrable_imp_measurable lebesgue_on_UNIV_eq by blast
     then show "{x \<in> T. f x \<noteq> 0} \<in> sets lebesgue"
       unfolding borel_measurable_vimage_open
       by (rule allE [where x = "-{0}"]) auto