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