diff -r 272ad6a47d6d -r 2d47c7d10b62 src/HOL/Codegenerator_Test/Code_Test_PolyML.thy
--- a/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy	Mon Sep 15 18:12:09 2014 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Test_PolyML.thy	Tue Sep 16 16:04:08 2014 +0200
@@ -8,6 +8,6 @@
 
 test_code "14 + 7 * -12 = (140 div -2 :: integer)" in PolyML
 
-eval_term "14 + 7 * -12 :: integer" in PolyML
+value [PolyML] "14 + 7 * -12 :: integer"
 
 end