--- a/src/HOL/Cardinals/Wellorder_Relation.thy	Wed Mar 05 18:28:57 2025 +0100
+++ b/src/HOL/Cardinals/Wellorder_Relation.thy	Tue Mar 11 10:20:44 2025 +0100
@@ -218,7 +218,7 @@
 next
   fix b assume "(suc B, b) \<in> r"
   thus "b \<in> Field r"
-    using REFL refl_on_def[of _ r] by auto
+    by (simp add: FieldI2)
 next
   fix a b
   assume 1: "(suc B, b) \<in> r" and 2: "a \<in> B"