diff -r 9b00f09f7721 -r 8f5add916a99 src/Pure/ML/ml_parse.ML
--- a/src/Pure/ML/ml_parse.ML	Sat Jul 23 16:37:17 2011 +0200
+++ b/src/Pure/ML/ml_parse.ML	Sat Jul 23 17:22:28 2011 +0200
@@ -53,14 +53,13 @@
   regular ||
   bad_input;
 
-fun do_fix_ints s =
-  Source.of_string s
-  |> ML_Lex.source
-  |> Source.source ML_Lex.stopper (Scan.bulk (!!! fix_int)) NONE
-  |> Source.exhaust
-  |> implode;
-
-val fix_ints = if ml_system_fix_ints then do_fix_ints else I;
+val fix_ints =
+  ML_System.is_smlnj ?
+   (Source.of_string #>
+    ML_Lex.source #>
+    Source.source ML_Lex.stopper (Scan.bulk (!!! fix_int)) NONE #>
+    Source.exhaust #>
+    implode);
 
 
 (* global use_context *)