1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Mar 12 21:28:10 2012 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Mar 12 21:34:43 2012 +0100
     1.3 @@ -3175,8 +3175,8 @@
     1.4      have "eventually (\<lambda>n. dist (x n) a < d) sequentially"
     1.5        using x(2) `d>0` by simp
     1.6      hence "eventually (\<lambda>n. (f \<circ> x) n \<in> T) sequentially"
     1.7 -    proof (rule eventually_elim1)
     1.8 -      fix n assume "dist (x n) a < d" thus "(f \<circ> x) n \<in> T"
     1.9 +    proof eventually_elim
    1.10 +      case (elim n) thus ?case
    1.11          using d x(1) `f a \<in> T` unfolding dist_nz[THEN sym] by auto
    1.12      qed
    1.13    }