1.1 --- a/src/HOL/BNF_Wellorder_Embedding.thy	Fri Feb 28 22:00:13 2014 +0100
     1.2 +++ b/src/HOL/BNF_Wellorder_Embedding.thy	Fri Feb 28 17:54:52 2014 +0100
     1.3 @@ -305,8 +305,7 @@
     1.4    (* Main proof *)
     1.5    show "bij_betw f (under r a) (under r' (f a))"
     1.6    proof(unfold bij_betw_def, auto)
     1.7 -    show  "inj_on f (under r a)"
     1.8 -    using * by (metis (no_types) under_Field subset_inj_on)
     1.9 +    show  "inj_on f (under r a)" by (rule subset_inj_on[OF * under_Field])
    1.10    next
    1.11      fix b assume "b \<in> under r a"
    1.12      thus "f b \<in> under r' (f a)"
    1.13 @@ -1035,8 +1034,7 @@
    1.14    {fix a assume ***: "a \<in> Field r"
    1.15     have "bij_betw f (under r a) (under r' (f a))"
    1.16     proof(unfold bij_betw_def, auto)
    1.17 -     show "inj_on f (under r a)"
    1.18 -     using 1 2 by (metis subset_inj_on)
    1.19 +     show "inj_on f (under r a)" using 1 2 subset_inj_on by blast
    1.20     next
    1.21       fix b assume "b \<in> under r a"
    1.22       hence "a \<in> Field r \<and> b \<in> Field r \<and> (b,a) \<in> r"