--- 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