src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy

   next
     assume r: ?R
     show ?L
     proof
       fix x assume x: "x \<in> H"
-      show "\<And>a b :: real. - a \<le> b \<Longrightarrow> b \<le> a \<Longrightarrow> \<bar>b\<bar> \<le> a"
+      show "- a \<le> b \<Longrightarrow> b \<le> a \<Longrightarrow> \<bar>b\<bar> \<le> a" for a b :: real
         by arith
       from \<open>linearform H h\<close> and H x
       have "- h x = h (- x)" by (rule linearform.neg [symmetric])
       also
       from H x have "- x \<in> H" by (rule vectorspace.neg_closed)