src/Pure/Tools/debugger.ML

     "Context.put_generic_context (SOME (Context.Proof ML_context))",
     "Context.put_generic_context (SOME ML_context)"];
 
 fun evaluate {SML, verbose} =
   ML_Context.eval
-    {SML_syntax = SML, SML_env = SML, exchange = false, redirect = false, verbose = verbose,
+    {SML = SML, exchange = false, redirect = false, verbose = verbose,
       debug = SOME false, writeln = writeln_message, warning = warning_message}
     Position.none;
 
 fun eval_setup thread_name index SML context =
   context