diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Library/Code_Char_chr.thy
--- a/src/HOL/Library/Code_Char_chr.thy	Mon Sep 06 22:58:06 2010 +0200
+++ b/src/HOL/Library/Code_Char_chr.thy	Tue Sep 07 10:05:19 2010 +0200
@@ -13,14 +13,14 @@
 
 lemma [code]:
   "nat_of_char = nat o int_of_char"
-  unfolding int_of_char_def by (simp add: expand_fun_eq)
+  unfolding int_of_char_def by (simp add: ext_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: expand_fun_eq)
+  unfolding char_of_int_def by (simp add: ext_iff)
 
 code_const int_of_char and char_of_int
   (SML "!(IntInf.fromInt o Char.ord)" and "!(Char.chr o IntInf.toInt)")