src/Pure/ML/ml_env.ML
changeset 48992 0518bf89c777
parent 36165 310a3f2f0e7e
child 56203 76c72f4d0667
--- a/src/Pure/ML/ml_env.ML	Wed Aug 29 11:31:07 2012 +0200
+++ b/src/Pure/ML/ml_env.ML	Wed Aug 29 11:48:45 2012 +0200
@@ -85,7 +85,7 @@
 val local_context: use_context =
  {tune_source = ML_Parse.fix_ints,
   name_space = name_space,
-  str_of_pos = Position.str_of oo Position.line_file,
+  str_of_pos = Position.here oo Position.line_file,
   print = writeln,
   error = error};