--- a/src/HOL/Hilbert_Choice.thy Mon Sep 13 08:43:48 2010 +0200
+++ b/src/HOL/Hilbert_Choice.thy Mon Sep 13 11:13:15 2010 +0200
@@ -138,7 +138,7 @@
qed
lemma inj_iff: "(inj f) = (inv f o f = id)"
-apply (simp add: o_def ext_iff)
+apply (simp add: o_def fun_eq_iff)
apply (blast intro: inj_on_inverseI inv_into_f_f)
done
@@ -178,7 +178,7 @@
by (simp add: inj_on_inv_into surj_range)
lemma surj_iff: "(surj f) = (f o inv f = id)"
-apply (simp add: o_def ext_iff)
+apply (simp add: o_def fun_eq_iff)
apply (blast intro: surjI surj_f_inv_f)
done