src/HOL/Analysis/Henstock_Kurzweil_Integration.thy

   have "(indicat_real (S \<union> T) has_integral 0) (cbox a b)"
     if S0: "(indicat_real S has_integral 0) (cbox a b)" 
       and  "(indicat_real T has_integral 0) (cbox a b)" for a b
   proof (subst has_integral_spike_eq[OF T])
     show "indicat_real S x = indicat_real (S \<union> T) x" if "x \<in> cbox a b - T" for x
-      by (metis Diff_iff Un_iff indicator_def that)
+      using that by (simp add: indicator_def)
     show "(indicat_real S has_integral 0) (cbox a b)"
       by (simp add: S0)
   qed
   with assms show ?thesis
     unfolding negligible_def by blast