--- a/src/HOL/String.thy Mon Sep 13 08:43:48 2010 +0200
+++ b/src/HOL/String.thy Mon Sep 13 11:13:15 2010 +0200
@@ -60,12 +60,12 @@
lemma char_case_nibble_pair [code, code_unfold]:
"char_case f = split f o nibble_pair_of_char"
- by (simp add: ext_iff split: char.split)
+ by (simp add: fun_eq_iff split: char.split)
lemma char_rec_nibble_pair [code, code_unfold]:
"char_rec f = split f o nibble_pair_of_char"
unfolding char_case_nibble_pair [symmetric]
- by (simp add: ext_iff split: char.split)
+ by (simp add: fun_eq_iff split: char.split)
syntax
"_Char" :: "xstr => char" ("CHR _")