--- 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
--- a/src/HOL/Library/Multiset_Order.thy Mon Feb 19 11:39:00 2024 +0100
+++ b/src/HOL/Library/Multiset_Order.thy Mon Feb 19 14:31:26 2024 +0100
@@ -652,7 +652,7 @@
by (metis image_mset_Diff image_mset_union)
next
obtain y where y: "\<forall>x. x \<in># X \<longrightarrow> y x \<in># Y \<and> x < y x"
- using ex_y by moura
+ using ex_y by metis
show "\<forall>fx. fx \<in># ?fX \<longrightarrow> (\<exists>fy. fy \<in># ?fY \<and> fx < fy)"
proof (intro allI impI)