diff -r 6f20a44c3cb1 -r 881bd98bddee src/HOL/Fun_Def.thy
--- a/src/HOL/Fun_Def.thy	Thu Aug 20 10:39:26 2020 +0100
+++ b/src/HOL/Fun_Def.thy	Fri Aug 21 12:42:57 2020 +0100
@@ -208,7 +208,7 @@
   by (auto simp: pair_less_def)
 
 lemma total_pair_less [iff]: "total_on A pair_less" and trans_pair_less [iff]: "trans pair_less"
-  by (auto simp: total_on_def pair_less_def antisym_def)
+  by (auto simp: total_on_def pair_less_def)
 
 text \<open>Introduction rules for \<open>pair_less\<close>/\<open>pair_leq\<close>\<close>
 lemma pair_leqI1: "a < b \<Longrightarrow> ((a, s), (b, t)) \<in> pair_leq"