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};