# HG changeset patch
# User haftmann
# Date 1241618465 -7200
# Node ID c1969f609bf759d3630866d1a1c42e05f3bf1a51
# Parent  f0c7607bb295668e8c6968e845096db6b2253c92
confine term setup to Eval serialiser

diff -r f0c7607bb295 -r c1969f609bf7 src/HOL/Library/Code_Char.thy
--- 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