src/HOL/Library/Code_Char.thy
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