diff -r 39f8051f71d4 -r 1c358879bfd3 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Sun Jan 22 23:29:34 2023 +0100
+++ b/src/HOL/Relation.thy	Mon Jan 23 13:31:07 2023 +0100
@@ -751,7 +751,7 @@
 abbreviation totalp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
   "totalp \<equiv> totalp_on UNIV"
 
-lemma totalp_on_refl_on_eq[pred_set_conv]: "totalp_on A (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> total_on A r"
+lemma totalp_on_total_on_eq[pred_set_conv]: "totalp_on A (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> total_on A r"
   by (simp add: totalp_on_def total_on_def)
 
 lemma total_onI [intro?]: