src/HOL/Nat.thy

--- a/src/HOL/Nat.thy	Mon Sep 06 22:58:06 2010 +0200
+++ b/src/HOL/Nat.thy	Tue Sep 07 10:05:19 2010 +0200
@@ -1360,7 +1360,7 @@
   by (induct n) simp_all
 
 lemma of_nat_eq_id [simp]: "of_nat = id"
-  by (auto simp add: expand_fun_eq)
+  by (auto simp add: ext_iff)
 
 
 subsection {* The Set of Natural Numbers *}