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