diff -r 06bce659d41b -r 53323937ee25 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Apr 13 17:00:57 2018 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sat Apr 14 09:23:00 2018 +0100
@@ -5258,7 +5258,7 @@
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
   assumes "f integrable_on S" "f integrable_on T" "negligible (S \<inter> T)"
   shows "integral (S \<union> T) f = integral S f + integral T f"
-  using has_integral_Un by (simp add: has_integral_Un assms integrable_integral integral_unique)
+  by (simp add: has_integral_Un assms integrable_integral integral_unique)
 
 lemma integrable_Un:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b :: banach"