--- a/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy Wed Jun 10 11:14:04 2015 +0200
+++ b/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy Wed Jun 10 11:14:46 2015 +0200
@@ -420,7 +420,7 @@
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])