diff -r 0f1e411a1448 -r a2ad5b824051 src/Pure/ML/ml_syntax.ML
--- a/src/Pure/ML/ml_syntax.ML	Mon Jan 10 15:30:17 2011 +0100
+++ b/src/Pure/ML/ml_syntax.ML	Mon Jan 10 15:45:46 2011 +0100
@@ -49,7 +49,7 @@
 
 val atomic = enclose "(" ")";
 
-val print_int = Int.toString;
+val print_int = string_of_int;
 
 fun print_pair f1 f2 (x, y) = "(" ^ f1 x ^ ", " ^ f2 y ^ ")";