--- a/src/HOL/Nat.thy Mon Sep 13 08:43:48 2010 +0200
+++ b/src/HOL/Nat.thy Mon Sep 13 11:13:15 2010 +0200
@@ -1360,7 +1360,7 @@
by (induct n) simp_all
lemma of_nat_eq_id [simp]: "of_nat = id"
- by (auto simp add: ext_iff)
+ by (auto simp add: fun_eq_iff)
subsection {* The Set of Natural Numbers *}