src/Pure/Tools/debugger.ML
changeset 60871 9b26f3118e40
parent 60869 878e32cf3131
child 60878 1f0d2bbcf38b
--- a/src/Pure/Tools/debugger.ML	Sat Aug 08 22:08:43 2015 +0200
+++ b/src/Pure/Tools/debugger.ML	Mon Aug 10 11:20:16 2015 +0200
@@ -152,6 +152,7 @@
     val evaluate_verbose = evaluate {SML = SML, verbose = true};
     val context1 = ML_Context.the_generic_context ()
       |> Context_Position.set_visible_generic false
+      |> Config.put_generic ML_Options.debugger false
       |> ML_Env.add_name_space {SML = SML}
           (ML_Debugger.debug_name_space (the_debug_state thread_name index));
     val context2 =