src/Pure/General/pretty.ML
changeset 62672 068b430e678f
parent 62667 254582abf067
child 62783 75ee05386b90
--- a/src/Pure/General/pretty.ML	Fri Mar 18 20:35:01 2016 +0100
+++ b/src/Pure/General/pretty.ML	Fri Mar 18 21:21:09 2016 +0100
@@ -394,9 +394,7 @@
 
 end;
 
-val _ =
-  PolyML.addPrettyPrinter (fn depth => fn _ => ML_Pretty.to_polyml o to_ML (depth * 2 + 1) o quote);
-
+val _ = PolyML.addPrettyPrinter (fn d => fn _ => ML_Pretty.to_polyml o to_ML (d + 1) o quote);
 val _ = PolyML.addPrettyPrinter (fn _ => fn _ => to_polyml o position);
 
 end;