--- 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)")