diff -r 9f36a31fe7ae -r a3e7a323780f src/HOL/Analysis/Retracts.thy
--- a/src/HOL/Analysis/Retracts.thy	Mon Feb 19 11:39:00 2024 +0100
+++ b/src/HOL/Analysis/Retracts.thy	Mon Feb 19 14:31:26 2024 +0100
@@ -1178,7 +1178,7 @@
       if "openin (top_of_set U) V" "T retract_of V" "U \<noteq> {}" for V
     using \<open>S homeomorphic T\<close> homeomorphic_locally homeomorphic_path_connectedness by blast
   obtain Ta where "(openin (top_of_set U) Ta \<and> T retract_of Ta)"
-    using ANR_def UT \<open>S homeomorphic T\<close> assms by moura
+    using ANR_def UT \<open>S homeomorphic T\<close> assms by atomize_elim (auto simp: choice)
   then show ?thesis
     using S \<open>U \<noteq> {}\<close> by blast
 qed