diff -r 3b36fc4916af -r 1249b998e377 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Fri Apr 17 17:32:11 2020 +0200
+++ b/src/HOL/Wellfounded.thy	Fri Apr 17 20:55:53 2020 +0100
@@ -580,8 +580,8 @@
 lemma less_than_iff [iff]: "((x,y) \<in> less_than) = (x<y)"
   by (simp add: less_than_def less_eq)
 
-lemma total_less_than: "total less_than"
-  using total_on_def by force
+lemma total_less_than: "total less_than" and total_on_less_than [simp]: "total_on A less_than"
+  using total_on_def by force+
 
 lemma wf_less: "wf {(x, y::nat). x < y}"
   by (rule Wellfounded.wellorder_class.wf)