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