src/HOL/Data_Structures/Sorted_Less.thy

--- a/src/HOL/Data_Structures/Sorted_Less.thy	Mon Dec 19 15:54:03 2022 +0100
+++ b/src/HOL/Data_Structures/Sorted_Less.thy	Mon Dec 19 16:00:49 2022 +0100
@@ -20,7 +20,7 @@
 
 declare
   sorted_wrt.simps(2)[simp del]
-  sorted_wrt1[simp] sorted_wrt2[OF transp_less, simp]
+  sorted_wrt1[simp] sorted_wrt2[OF transp_on_less, simp]
 
 lemma sorted_cons: "sorted (x#xs) \<Longrightarrow> sorted xs"
 by(simp add: sorted_wrt_Cons)