diff -r a594429637fd -r fdd6989cc8a0 src/Pure/ML/ml_env.ML
--- a/src/Pure/ML/ml_env.ML	Wed Feb 17 21:08:18 2016 +0100
+++ b/src/Pure/ML/ml_env.ML	Wed Feb 17 23:06:24 2016 +0100
@@ -163,8 +163,7 @@
   end;
 
 val local_context: use_context =
- {tune_source = ML_Parse.fix_ints,
-  name_space = name_space {SML = false, exchange = false},
+ {name_space = name_space {SML = false, exchange = false},
   str_of_pos = Position.here oo Position.line_file,
   print = writeln,
   error = error};