src/HOL/Cardinals/Cardinal_Order_Relation.thy

 proof
   assume "natLeq_on m \<le>o natLeq_on n"
   then obtain f where "inj_on f {x. x < m} \<and> f ` {x. x < m} \<le> {x. x < n}"
   unfolding ordLeq_def using
     embed_inj_on[OF natLeq_on_Well_order[of m], of "natLeq_on n", unfolded Field_natLeq_on]
-     embed_Field[OF natLeq_on_Well_order[of m], of "natLeq_on n", unfolded Field_natLeq_on] by blast
+     embed_Field Field_natLeq_on by blast
   thus "m \<le> n" using atLeastLessThan_less_eq2
     unfolding atLeast_0 atLeastLessThan_def lessThan_def Int_UNIV_left by blast
 next
   assume "m \<le> n"
   hence "inj_on id {0..<m} \<and> id ` {0..<m} \<le> {0..<n}" unfolding inj_on_def by auto