diff -r 0b5efc6de385 -r b1d57dd345e1 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Mon Dec 19 14:09:37 2022 +0100
+++ b/src/HOL/Fun.thy	Tue Dec 20 17:59:44 2022 +0000
@@ -300,11 +300,17 @@
     using lin [of x y] ne by (force simp: dual_order.order_iff_strict)
 qed
 
+lemma linorder_inj_onI':
+  fixes A :: "'a :: linorder set"
+  assumes "\<And>i j. i \<in> A \<Longrightarrow> j \<in> A \<Longrightarrow> i < j \<Longrightarrow> f i \<noteq> f j"
+  shows   "inj_on f A"
+  by (intro linorder_inj_onI) (auto simp add: assms)
+
 lemma linorder_injI:
   assumes "\<And>x y::'a::linorder. x < y \<Longrightarrow> f x \<noteq> f y"
   shows "inj f"
     \<comment> \<open>Courtesy of Stephan Merz\<close>
-using assms by (auto intro: linorder_inj_onI linear)
+using assms by (simp add: linorder_inj_onI')
 
 lemma inj_on_image_Pow: "inj_on f A \<Longrightarrow>inj_on (image f) (Pow A)"
   unfolding Pow_def inj_on_def by blast