src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy

 lemma inj_injf_max: "\<forall>x. \<exists>y \<in> E. x < y \<Longrightarrow> inj (\<lambda>n. injf_max n E)"
   apply (rule inj_onI)
   apply (rule ccontr)
   apply auto
   apply (drule injf_max_order_preserving2)
-  apply (metis linorder_antisym_conv3 order_less_le)
+  apply (metis antisym_conv3 order_less_le)
   done
 
 lemma infinite_set_has_order_preserving_inj:
   "E \<noteq> {} \<Longrightarrow> \<forall>x. \<exists>y \<in> E. x < y \<Longrightarrow> \<exists>f. range f \<subseteq> E \<and> inj f \<and> (\<forall>m. f m < f (Suc m))"
   for E :: "'a::order set" and f :: "nat \<Rightarrow> 'a"