--- a/src/HOL/Hilbert_Choice.thy Mon Sep 06 22:58:06 2010 +0200
+++ b/src/HOL/Hilbert_Choice.thy Tue Sep 07 10:05:19 2010 +0200
@@ -138,7 +138,7 @@
qed
lemma inj_iff: "(inj f) = (inv f o f = id)"
-apply (simp add: o_def expand_fun_eq)
+apply (simp add: o_def ext_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 expand_fun_eq)
+apply (simp add: o_def ext_iff)
apply (blast intro: surjI surj_f_inv_f)
done