src/Pure/ML/ml_print_depth0.ML
2016-04-07 wenzelm 2016-04-07 simplified default print_depth: context is usually available, in contrast to 0d295e339f52;
2016-04-05 wenzelm 2016-04-05 clarified modules -- simplified bootstrap;