diff -r e1bd8a54c40f -r d7728f65b353 src/HOL/Library/Code_Char_chr.thy
--- a/src/HOL/Library/Code_Char_chr.thy	Mon Sep 13 08:43:48 2010 +0200
+++ b/src/HOL/Library/Code_Char_chr.thy	Mon Sep 13 11:13:15 2010 +0200
@@ -13,14 +13,14 @@
 
 lemma [code]:
   "nat_of_char = nat o int_of_char"
-  unfolding int_of_char_def by (simp add: ext_iff)
+  unfolding int_of_char_def by (simp add: fun_eq_iff)
 
 definition
   "char_of_int = char_of_nat o nat"
 
 lemma [code]:
   "char_of_nat = char_of_int o int"
-  unfolding char_of_int_def by (simp add: ext_iff)
+  unfolding char_of_int_def by (simp add: fun_eq_iff)
 
 code_const int_of_char and char_of_int
   (SML "!(IntInf.fromInt o Char.ord)" and "!(Char.chr o IntInf.toInt)")