# HG changeset patch
# User haftmann
# Date 1250257013 -7200
# Node ID 3186fa3a4f88bd71d3d4dd06bde1e3ab74e77403
# Parent  9b74d0339c443619fb42b9411bd0edb19f384607
corrected Pair to Char

diff -r 9b74d0339c44 -r 3186fa3a4f88 src/HOL/Code_Eval.thy
--- a/src/HOL/Code_Eval.thy	Wed Aug 12 00:26:01 2009 +0200
+++ b/src/HOL/Code_Eval.thy	Fri Aug 14 15:36:53 2009 +0200
@@ -134,7 +134,7 @@
 
 lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]: "Code_Eval.term_of c =
     (let (n, m) = nibble_pair_of_char c
-  in Code_Eval.App (Code_Eval.App (Code_Eval.Const (STR ''Pair'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
+  in Code_Eval.App (Code_Eval.App (Code_Eval.Const (STR ''String.char.Char'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
     (Code_Eval.term_of n)) (Code_Eval.term_of m))"
   by (subst term_of_anything) rule