diff -r 0d56854096ba -r 5ebaa364d8ab src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Sat Apr 26 13:25:44 2014 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Sat Apr 26 13:25:45 2014 +0200
@@ -235,11 +235,11 @@
 lemma image_surj_f_inv_f: "surj f ==> f ` (inv f ` A) = A"
 by (simp add: image_eq_UN surj_f_inv_f)
 
-lemma image_inv_f_f: "inj f ==> (inv f) ` (f ` A) = A"
-by (simp add: image_eq_UN)
+lemma image_inv_f_f: "inj f ==> inv f ` (f ` A) = A"
+  by (simp add: image_eq_UN)
 
-lemma inv_image_comp: "inj f ==> inv f ` (f`X) = X"
-by (auto simp add: image_def)
+lemma inv_image_comp: "inj f ==> inv f ` (f ` X) = X"
+  by (fact image_inv_f_f)
 
 lemma bij_image_Collect_eq: "bij f ==> f ` Collect P = {y. P (inv f y)}"
 apply auto