src/HOL/Library/Efficient_Nat.thy
changeset 39302 d7728f65b353
parent 39272 0b61951d2682
child 39781 2053638a2bf2
--- a/src/HOL/Library/Efficient_Nat.thy	Mon Sep 13 08:43:48 2010 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Mon Sep 13 11:13:15 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: ext_iff dest!: gr0_implies_Suc)
+  by (auto simp add: fun_eq_iff dest!: gr0_implies_Suc)
 
 
 subsection {* Preprocessors *}