diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Mon Sep 06 22:58:06 2010 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Tue Sep 07 10:05:19 2010 +0200
@@ -79,7 +79,7 @@
 
 lemma [code, code_unfold]:
   "nat_case = (\<lambda>f g n. if n = 0 then f else g (n - 1))"
-  by (auto simp add: expand_fun_eq dest!: gr0_implies_Suc)
+  by (auto simp add: ext_iff dest!: gr0_implies_Suc)
 
 
 subsection {* Preprocessors *}