src/Pure/Pure.thy

 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>SML_export\<close> "evaluate SML within Isabelle/ML environment"
     (Parse.ML_source >> (fn source =>
       let
         val flags: ML_Compiler.flags =
-          {SML = true, exchange = true, redirect = false, verbose = true,
+          {read = SOME ML_Env.SML, write = NONE, redirect = false, verbose = true,
             debug = NONE, writeln = writeln, warning = warning};
       in
         Toplevel.theory
           (Context.theory_map (ML_Context.exec (fn () => ML_Context.eval_source flags source)))
       end));

 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>SML_import\<close> "evaluate Isabelle/ML within SML environment"
     (Parse.ML_source >> (fn source =>
       let
         val flags: ML_Compiler.flags =
-          {SML = false, exchange = true, redirect = false, verbose = true,
+          {read = NONE, write = SOME ML_Env.SML, redirect = false, verbose = true,
             debug = NONE, writeln = writeln, warning = warning};
       in
         Toplevel.generic_theory
           (ML_Context.exec (fn () => ML_Context.eval_source flags source) #>
             Local_Theory.propagate_ml_env)

   Outer_Syntax.command ("ML_export", \<^here>)
     "ML text within theory or local theory, and export to bootstrap environment"
     (Parse.ML_source >> (fn source =>
       Toplevel.generic_theory (fn context =>
         context
-        |> ML_Env.set_global true
+        |> Config.put_generic ML_Env.ML_write_global true
         |> ML_Context.exec (fn () =>
             ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source)
-        |> ML_Env.restore_global context
+        |> Config.put_generic ML_Env.ML_write_global
+            (Config.get_generic context ML_Env.ML_write_global)
         |> Local_Theory.propagate_ml_env)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>ML_prf\<close> "ML text within proof"
     (Parse.ML_source >> (fn source =>

     from conj show "PROP A" by (rule conjunctionD1)
     from conj show "PROP B" by (rule conjunctionD2)
   qed
 qed
 
+declare [[ML_write_global = false]]
+
 end