--- 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 ^ ")";