src/Pure/ML/ml_env.ML
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};