--- a/src/HOL/BNF_Wellorder_Constructions.thy	Mon Mar 17 11:30:39 2025 +0100
+++ b/src/HOL/BNF_Wellorder_Constructions.thy	Mon Mar 17 16:29:48 2025 +0100
@@ -847,7 +847,7 @@
     moreover
     {assume Case2: "\<not> Well_order r0"
       hence "?R = {}" unfolding ordLess_def by auto
-      hence "wf ?R" using wf_empty by simp
+      hence "wf ?R" by simp
     }
     ultimately have "wf ?R" by blast
   }