src/Pure/System/options.ML

--- a/src/Pure/System/options.ML	Tue Apr 05 20:05:05 2016 +0200
+++ b/src/Pure/System/options.ML	Tue Apr 05 20:51:37 2016 +0200
@@ -222,6 +222,6 @@
       end);
 
 val _ = load_default ();
-val _ = ML_Pretty.print_depth (default_int "ML_print_depth");
+val _ = ML_Print_Depth.set_print_depth (default_int "ML_print_depth");
 
 end;