diff -r 741560a5283b -r 1cec457e0a03 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Tue Apr 05 20:05:05 2016 +0200
+++ b/src/Pure/ML/ml_context.ML	Tue Apr 05 20:51:37 2016 +0200
@@ -118,8 +118,8 @@
      \val ML_context = Context_Position.set_visible " ^ Bool.toString visible ^
      " (Context.the_local_context ());\n\
      \val ML_print_depth =\n\
-     \  let val default = ML_Options.get_print_depth ()\n\
-     \  in fn () => ML_Options.get_print_depth_default default end;\n"),
+     \  let val default = ML_Print_Depth.get_print_depth ()\n\
+     \  in fn () => ML_Print_Depth.get_print_depth_default default end;\n"),
    ML_Lex.tokenize "end;");
 
 fun reset_env name = ML_Lex.tokenize ("structure " ^ name ^ " = struct end");