changeset 31046 | c1969f609bf7 |
parent 30663 | 0b6aff7451b2 |
child 31053 | b7e1c065b6e4 |
1.1 --- a/src/HOL/Library/Code_Char.thy Wed May 06 16:01:05 2009 +0200 1.2 +++ b/src/HOL/Library/Code_Char.thy Wed May 06 16:01:05 2009 +0200 1.3 @@ -33,6 +33,6 @@ 1.4 (Haskell infixl 4 "==") 1.5 1.6 code_const "Code_Eval.term_of \<Colon> char \<Rightarrow> term" 1.7 - (SML "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))") 1.8 + (Eval "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))") 1.9 1.10 end