src/Pure/ML/ml_pretty.ML
changeset 62672 068b430e678f
parent 62663 bea354f6ff21
child 62711 09df6a51ad3c
     1.1 --- a/src/Pure/ML/ml_pretty.ML	Fri Mar 18 20:35:01 2016 +0100
     1.2 +++ b/src/Pure/ML/ml_pretty.ML	Fri Mar 18 21:21:09 2016 +0100
     1.3 @@ -96,7 +96,7 @@
     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 10;
     1.8 +  val _ = print_depth 20;
     1.9  end;
    1.10  
    1.11