diff -r a7d9e34c85e6 -r 4352d0ff165a src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Mon Nov 21 18:24:55 2022 +0100
+++ b/src/HOL/Wellfounded.thy	Mon Nov 21 14:11:30 2022 +0100
@@ -75,7 +75,7 @@
   using wf_irrefl [OF assms] by (auto simp add: irrefl_def)
 
 lemma wfP_imp_irreflp: "wfP r \<Longrightarrow> irreflp r"
-  by (rule wf_imp_irrefl[to_pred])
+  by (rule wf_imp_irrefl[to_pred, folded top_set_def])
 
 lemma wf_wellorderI:
   assumes wf: "wf {(x::'a::ord, y). x < y}"