src/HOL/Nat.thy

--- a/src/HOL/Nat.thy	Wed Jul 11 23:24:25 2018 +0100
+++ b/src/HOL/Nat.thy	Thu Jul 12 17:22:39 2018 +0100
@@ -2093,7 +2093,7 @@
 
 lemma inj_on_diff_nat:
   fixes k :: nat
-  assumes "\<forall>n \<in> N. k \<le> n"
+  assumes "\<And>n. n \<in> N \<Longrightarrow> k \<le> n"
   shows "inj_on (\<lambda>n. n - k) N"
 proof (rule inj_onI)
   fix x y