tuned signature;

--- a/src/Pure/Pure.thy	Tue Aug 28 11:13:33 2018 +0200
+++ b/src/Pure/Pure.thy	Tue Aug 28 11:22:04 2018 +0200
@@ -200,10 +200,8 @@
         |> 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 _ =

--- a/src/Pure/config.ML	Tue Aug 28 11:13:33 2018 +0200
+++ b/src/Pure/config.ML	Tue Aug 28 11:22:04 2018 +0200
@@ -18,12 +18,15 @@
   val get: Proof.context -> 'a T -> 'a
   val map: 'a T -> ('a -> 'a) -> Proof.context -> Proof.context
   val put: 'a T -> 'a -> Proof.context -> Proof.context
+  val restore: 'a T -> Proof.context -> Proof.context -> Proof.context
   val get_global: theory -> 'a T -> 'a
   val map_global: 'a T -> ('a -> 'a) -> theory -> theory
   val put_global: 'a T -> 'a -> theory -> theory
+  val restore_global: 'a T -> theory -> theory -> theory
   val get_generic: Context.generic -> 'a T -> 'a
   val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic
   val put_generic: 'a T -> 'a -> Context.generic -> Context.generic
+  val restore_generic: 'a T -> Context.generic -> Context.generic -> Context.generic
   val declare: string * Position.T -> (Context.generic -> value) -> raw
   val declare_option: string * Position.T -> raw
   val name_of: 'a T -> string
@@ -91,14 +94,17 @@
 fun get_generic context (Config {get_value, ...}) = get_value context;
 fun map_generic (Config {map_value, ...}) f context = map_value f context;
 fun put_generic config value = map_generic config (K value);
+fun restore_generic config context = put_generic config (get_generic context config);
 
 fun get_ctxt ctxt = get_generic (Context.Proof ctxt);
 fun map_ctxt config f = Context.proof_map (map_generic config f);
 fun put_ctxt config value = map_ctxt config (K value);
+fun restore_ctxt config ctxt = put_ctxt config (get_ctxt ctxt config);
 
 fun get_global thy = get_generic (Context.Theory thy);
 fun map_global config f = Context.theory_map (map_generic config f);
 fun put_global config value = map_global config (K value);
+fun restore_global config thy = put_global config (get_global thy config);
 
 
 (* context information *)
@@ -145,5 +151,6 @@
 val get = get_ctxt;
 val map = map_ctxt;
 val put = put_ctxt;
+val restore = restore_ctxt;
 
 end;