--- 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 *)