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