diff -r 3fe7242f8346 -r 599ff65b85e2 src/HOL/Code_Evaluation.thy
--- a/src/HOL/Code_Evaluation.thy	Fri Feb 15 15:22:16 2013 +0100
+++ b/src/HOL/Code_Evaluation.thy	Fri Feb 15 11:47:33 2013 +0100
@@ -119,11 +119,10 @@
   = Code_Evaluation.term_of" ..
 
 lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]:
-  "Code_Evaluation.term_of c =
-    (let (n, m) = nibble_pair_of_char c
-  in Code_Evaluation.App (Code_Evaluation.App
+  "Code_Evaluation.term_of c = (case c of Char x y \<Rightarrow>
+   Code_Evaluation.App (Code_Evaluation.App
     (Code_Evaluation.Const (STR ''String.char.Char'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
-      (Code_Evaluation.term_of n)) (Code_Evaluation.term_of m))"
+      (Code_Evaluation.term_of x)) (Code_Evaluation.term_of y))"
   by (subst term_of_anything) rule 
 
 code_type "term"