src/Pure/Tools/debugger.ML
changeset 68820 2e4df245754e
parent 68816 5a53724fe247
child 68821 877534be1930
--- a/src/Pure/Tools/debugger.ML	Mon Aug 27 17:26:14 2018 +0200
+++ b/src/Pure/Tools/debugger.ML	Mon Aug 27 17:30:13 2018 +0200
@@ -132,12 +132,10 @@
     "Context.put_generic_context (SOME ML_context)"];
 
 fun evaluate {SML, verbose} =
-  let val env = ML_Env.make_standard SML in
-    ML_Context.eval
-      {read = SOME env, write = SOME env, redirect = false, verbose = verbose,
-        debug = SOME false, writeln = writeln_message, warning = warning_message}
-      Position.none
-  end;
+  ML_Context.eval
+    {environment = ML_Env.make_standard SML, redirect = false, verbose = verbose,
+      debug = SOME false, writeln = writeln_message, warning = warning_message}
+    Position.none;
 
 fun eval_setup thread_name index SML context =
   context