diff -r 741560a5283b -r 1cec457e0a03 src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Tue Apr 05 20:05:05 2016 +0200
+++ b/src/Pure/ML/ml_compiler.ML	Tue Apr 05 20:51:37 2016 +0200
@@ -199,7 +199,7 @@
 
     (* results *)
 
-    val depth = FixedInt.fromInt (ML_Options.get_print_depth ());
+    val depth = FixedInt.fromInt (ML_Print_Depth.get_print_depth ());
 
     fun apply_result {fixes, types, signatures, structures, functors, values} =
       let
@@ -258,7 +258,7 @@
       PolyML.Compiler.CPLineNo (the_default 0 o Position.line_of o get_pos),
       PolyML.Compiler.CPLineOffset (the_default 0 o Position.offset_of o get_pos),
       PolyML.Compiler.CPFileName location_props,
-      PolyML.Compiler.CPPrintDepth ML_Options.get_print_depth,
+      PolyML.Compiler.CPPrintDepth ML_Print_Depth.get_print_depth,
       PolyML.Compiler.CPCompilerResultFun result_fun,
       PolyML.Compiler.CPPrintInAlphabeticalOrder false,
       PolyML.Compiler.CPDebug debug];