--- a/src/Pure/ML/ml_pretty.ML Sat Mar 26 12:17:02 2016 +0100
+++ b/src/Pure/ML/ml_pretty.ML Sat Mar 26 12:22:15 2016 +0100
@@ -96,7 +96,6 @@
in
fun get_print_depth () = ! depth;
fun print_depth n = (depth := n; PolyML.print_depth n);
- val _ = print_depth 20;
end;