Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
corrected Pair to Char
authorhaftmann
Fri, 14 Aug 2009 15:36:53 +0200
changeset 32371 3186fa3a4f88
parent 32365 9b74d0339c44
child 32372 b0d2b49bfaed
corrected Pair to Char
src/HOL/Code_Eval.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle