diff -r f0d2609c4cdc -r 159b0c88b4a4 src/HOL/BNF_Constructions_on_Wellorders.thy
--- a/src/HOL/BNF_Constructions_on_Wellorders.thy	Tue Mar 18 10:12:58 2014 +0100
+++ b/src/HOL/BNF_Constructions_on_Wellorders.thy	Tue Mar 18 11:47:59 2014 +0100
@@ -894,8 +894,8 @@
 "dir_image r f = {(f a, f b)| a b. (a,b) \<in> r}"
 
 lemma dir_image_Field:
-"Field(dir_image r f) \<le> f ` (Field r)"
-unfolding dir_image_def Field_def by auto
+"Field(dir_image r f) = f ` (Field r)"
+unfolding dir_image_def Field_def Range_def Domain_def by fast
 
 lemma dir_image_minus_Id:
 "inj_on f (Field r) \<Longrightarrow> (dir_image r f) - Id = dir_image (r - Id) f"
@@ -965,7 +965,7 @@
   fix a' b'
   assume "a' \<in> Field (dir_image r f)" "b' \<in> Field (dir_image r f)"
   then obtain a and b where 1: "a \<in> Field r \<and> b \<in> Field r \<and> f a = a' \<and> f b = b'"
-  using dir_image_Field[of r f] by blast
+    unfolding dir_image_Field[of r f] by blast
   moreover assume "a' \<noteq> b'"
   ultimately have "a \<noteq> b" using INJ unfolding inj_on_def by auto
   hence "(a,b) \<in> r \<or> (b,a) \<in> r" using 1 TOT unfolding total_on_def by auto
@@ -984,10 +984,9 @@
   fix A'::"'b set"
   assume SUB: "A' \<le> Field(dir_image r f)" and NE: "A' \<noteq> {}"
   obtain A where A_def: "A = {a \<in> Field r. f a \<in> A'}" by blast
-  have "A \<noteq> {} \<and> A \<le> Field r"
-  using A_def dir_image_Field[of r f] SUB NE by blast
+  have "A \<noteq> {} \<and> A \<le> Field r" using A_def SUB NE by (auto simp: dir_image_Field)
   then obtain a where 1: "a \<in> A \<and> (\<forall>b \<in> A. (b,a) \<notin> r)"
-  using WF unfolding wf_eq_minimal2 by blast
+  using spec[OF WF[unfolded wf_eq_minimal2], of A] by blast
   have "\<forall>b' \<in> A'. (b',f a) \<notin> dir_image r f"
   proof(clarify)
     fix b' assume *: "b' \<in> A'" and **: "(b',f a) \<in> dir_image r f"
@@ -1010,14 +1009,9 @@
   subset_inj_on[of f "Field r" "Field(r - Id)"]
   mono_Field[of "r - Id" r] by auto
 
-lemma dir_image_Field2:
-"Refl r \<Longrightarrow> Field(dir_image r f) = f ` (Field r)"
-unfolding Field_def dir_image_def refl_on_def Domain_def Range_def by blast
-
 lemma dir_image_bij_betw:
-"\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> bij_betw f (Field r) (Field (dir_image r f))"
-unfolding bij_betw_def
-by (simp add: dir_image_Field2 order_on_defs)
+"\<lbrakk>inj_on f (Field r)\<rbrakk> \<Longrightarrow> bij_betw f (Field r) (Field (dir_image r f))"
+unfolding bij_betw_def by (simp add: dir_image_Field order_on_defs)
 
 lemma dir_image_compat:
 "compat r (dir_image r f) f"