diff -r f5989a2c1f67 -r 02c2860fcf30 src/Pure/ML/ml_compiler_polyml.ML
--- a/src/Pure/ML/ml_compiler_polyml.ML	Thu Jul 16 11:10:57 2015 +0200
+++ b/src/Pure/ML/ml_compiler_polyml.ML	Thu Jul 16 11:38:18 2015 +0200
@@ -183,7 +183,8 @@
       PolyML.Compiler.CPFileName location_props,
       PolyML.Compiler.CPPrintDepth ML_Options.get_print_depth,
       PolyML.Compiler.CPCompilerResultFun result_fun,
-      PolyML.Compiler.CPPrintInAlphabeticalOrder false];
+      PolyML.Compiler.CPPrintInAlphabeticalOrder false] @
+     ml_debugger_parameters (ML_Options.debugger_enabled opt_context);
     val _ =
       (while not (List.null (! input_buffer)) do
         PolyML.compiler (get, parameters) ())