--- a/src/HOL/String.thy Mon Sep 06 22:58:06 2010 +0200
+++ b/src/HOL/String.thy Tue Sep 07 10:05:19 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: expand_fun_eq split: char.split)
+ by (simp add: ext_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: expand_fun_eq split: char.split)
+ by (simp add: ext_iff split: char.split)
syntax
"_Char" :: "xstr => char" ("CHR _")