1.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Nov 05 09:44:57 2013 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Nov 05 09:44:58 2013 +0100
     1.3 @@ -660,7 +660,7 @@
     1.4      assume "S \<noteq> {}"
     1.5      { assume ex: "\<exists>B. \<forall>x\<in>S. B \<le> x"
     1.6        then have *: "\<forall>x\<in>S. Inf S \<le> x"
     1.7 -        using cInf_lower_EX[of _ S] ex by metis
     1.8 +        using cInf_lower[of _ S] ex by (metis bdd_below_def)
     1.9        then have "Inf S \<in> S"
    1.10          apply (subst closed_contains_Inf)
    1.11          using ex `S \<noteq> {}` `closed S`