src/Pure/ML/ml_env.ML
changeset 62493 dd154240a53c
parent 62354 fdd6989cc8a0
child 62494 b90109b2487c
--- 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};