1.1 --- a/src/HOL/Library/Code_Char_chr.thy	Mon Sep 13 08:43:48 2010 +0200
     1.2 +++ b/src/HOL/Library/Code_Char_chr.thy	Mon Sep 13 11:13:15 2010 +0200
     1.3 @@ -13,14 +13,14 @@
     1.4  
     1.5  lemma [code]:
     1.6    "nat_of_char = nat o int_of_char"
     1.7 -  unfolding int_of_char_def by (simp add: ext_iff)
     1.8 +  unfolding int_of_char_def by (simp add: fun_eq_iff)
     1.9  
    1.10  definition
    1.11    "char_of_int = char_of_nat o nat"
    1.12  
    1.13  lemma [code]:
    1.14    "char_of_nat = char_of_int o int"
    1.15 -  unfolding char_of_int_def by (simp add: ext_iff)
    1.16 +  unfolding char_of_int_def by (simp add: fun_eq_iff)
    1.17  
    1.18  code_const int_of_char and char_of_int
    1.19    (SML "!(IntInf.fromInt o Char.ord)" and "!(Char.chr o IntInf.toInt)")