confine term setup to Eval serialiser
authorhaftmann
Wed May 06 16:01:05 2009 +0200 (2009-05-06)
changeset 31046c1969f609bf7
parent 31045 f0c7607bb295
child 31047 c13b0406c039
confine term setup to Eval serialiser
src/HOL/Library/Code_Char.thy
     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