src/Pure/ML/ml_pretty.ML
changeset 62711 09df6a51ad3c
parent 62672 068b430e678f
child 62784 0371c369ab1d
     1.1 --- a/src/Pure/ML/ml_pretty.ML	Sat Mar 26 12:17:02 2016 +0100
     1.2 +++ b/src/Pure/ML/ml_pretty.ML	Sat Mar 26 12:22:15 2016 +0100
     1.3 @@ -96,7 +96,6 @@
     1.4  in
     1.5    fun get_print_depth () = ! depth;
     1.6    fun print_depth n = (depth := n; PolyML.print_depth n);
     1.7 -  val _ = print_depth 20;
     1.8  end;
     1.9  
    1.10