diff -r e1bd8a54c40f -r d7728f65b353 src/HOL/String.thy
--- 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 _")