src/HOL/Analysis/Abstract_Topology.thy

--- a/src/HOL/Analysis/Abstract_Topology.thy	Wed Aug 14 19:50:23 2019 +0200
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Thu Aug 15 16:11:56 2019 +0100
@@ -3985,7 +3985,7 @@
   ultimately
   have "\<forall>\<^sub>F x in at a within T. f x = g x"
     by eventually_elim (auto simp: \<open>S = _\<close> eq)
-  then show ?thesis using f
+  with f show ?thesis
     by (rule Lim_transform_eventually)
 qed