src/HOL/Wellfounded.thy

--- a/src/HOL/Wellfounded.thy	Fri Mar 21 14:21:44 2025 +0100
+++ b/src/HOL/Wellfounded.thy	Fri Mar 21 15:20:13 2025 +0100
@@ -524,7 +524,7 @@
 text \<open>Well-foundedness of subsets\<close>
 
 lemma wf_subset: "wf r \<Longrightarrow> p \<subseteq> r \<Longrightarrow> wf p"
-  by (simp add: wf_eq_minimal) fast
+  using wf_on_antimono[OF subset_UNIV, unfolded le_bool_def] ..
 
 lemmas wfp_subset = wf_subset [to_pred]