src/HOL/Wellfounded.thy

--- a/src/HOL/Wellfounded.thy	Sun Dec 18 13:53:05 2022 +0100
+++ b/src/HOL/Wellfounded.thy	Sun Dec 18 14:03:43 2022 +0100
@@ -604,7 +604,7 @@
   using irrefl_def by blast
 
 lemma asym_less_than: "asym less_than"
-  by (simp add: asym.simps irrefl_less_than)
+  by (rule asymI) simp
 
 lemma total_less_than: "total less_than" and total_on_less_than [simp]: "total_on A less_than"
   using total_on_def by force+