src/Pure/Pure.thy

         context
         |> Config.put_generic ML_Env.ML_environment ML_Env.Isabelle
         |> 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)
-        |> Config.put_generic ML_Env.ML_write_global
-            (Config.get_generic context ML_Env.ML_write_global)
-        |> Config.put_generic ML_Env.ML_environment
-            (Config.get_generic context ML_Env.ML_environment)
+        |> Config.restore_generic ML_Env.ML_write_global context
+        |> Config.restore_generic ML_Env.ML_environment context
         |> Local_Theory.propagate_ml_env)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>ML_prf\<close> "ML text within proof"
     (Parse.ML_source >> (fn source =>