diff -r 0e53fade87fe -r dd154240a53c src/Pure/ML/ml_env.ML
--- a/src/Pure/ML/ml_env.ML	Tue Mar 01 21:00:38 2016 +0100
+++ b/src/Pure/ML/ml_env.ML	Tue Mar 01 21:10:29 2016 +0100
@@ -164,7 +164,7 @@
 
 val local_context: use_context =
  {name_space = name_space {SML = false, exchange = false},
-  str_of_pos = Position.here oo Position.line_file,
+  here = Position.here oo Position.line_file,
   print = writeln,
   error = error};