diff -r 2d2b5a8e8d59 -r fcf3b891ccb1 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