diff -r 91e451bc0f1f -r 16a8991ab398 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Thu Apr 27 11:06:47 2017 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Thu Apr 27 15:59:00 2017 +0100
@@ -683,7 +683,7 @@
     by (simp add: AE_iff_measurable)
   show ?thesis
   proof (rule has_integral_spike_eq[symmetric])
-    show "\<forall>x\<in>\<Omega> - N. f x = g x" using N(3) by auto
+    show "\<And>x. x\<in>\<Omega> - N \<Longrightarrow> f x = g x" using N(3) by auto
     show "negligible N"
       unfolding negligible_def
     proof (intro allI)
@@ -2246,7 +2246,7 @@
   proof
     show "(\<lambda>x. norm (g x)) integrable_on s"
       using le norm_ge_zero[of "f _"]
-      by (intro integrable_spike_finite[OF _ _ g, where s="{}"])
+      by (intro integrable_spike_finite[OF _ _ g, of "{}"])
          (auto intro!: abs_of_nonneg intro: order_trans simp del: norm_ge_zero)
   qed fact
   show "set_borel_measurable lebesgue s f"
@@ -2266,9 +2266,9 @@
     unfolding absolutely_integrable_on_def
   proof
     show "(\<lambda>x. norm (h x)) integrable_on s"
-    proof (intro integrable_spike_finite[OF _ _ h, where s="{}"] ballI)
+    proof (intro integrable_spike_finite[OF _ _ h, of "{}"] ballI)
       fix x assume "x \<in> s - {}" then show "norm (h x) = h x"
-        using order_trans[OF norm_ge_zero le[THEN bspec, of x]] by auto
+        by (metis Diff_empty abs_of_nonneg bot_set_def le norm_ge_zero order_trans real_norm_def)
     qed auto
   qed fact
   have 2: "set_borel_measurable lebesgue s (f k)" for k