src/HOL/Hilbert_Choice.thy

--- a/src/HOL/Hilbert_Choice.thy	Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Mon Sep 12 07:55:43 2011 +0200
@@ -148,7 +148,7 @@
 
 lemma inv_into_image_cancel[simp]:
   "inj_on f A ==> S <= A ==> inv_into A f ` f ` S = S"
-by(fastsimp simp: image_def)
+by(fastforce simp: image_def)
 
 lemma inj_imp_surj_inv: "inj f ==> surj (inv f)"
 by (blast intro!: surjI inv_into_f_f)