changeset 62716 | d80b9f4990e4 |
parent 62657 | cdd6db02eae8 |
child 62839 | ea9f12e422c7 |
--- a/src/Pure/ML/ml_env.ML Sat Mar 26 14:27:58 2016 +0100 +++ b/src/Pure/ML/ml_env.ML Sat Mar 26 16:14:46 2016 +0100 @@ -164,6 +164,7 @@ val context: ML_Compiler0.context = {name_space = make_name_space {SML = false, exchange = false}, + print_depth = NONE, here = Position.here oo Position.line_file, print = writeln, error = error};