src/Pure/Pure.thy
changeset 68827 1286ca9dfd26
parent 68826 deefe5837120
child 68876 cefaac3d24ff
     1.1 --- a/src/Pure/Pure.thy	Tue Aug 28 11:13:33 2018 +0200
     1.2 +++ b/src/Pure/Pure.thy	Tue Aug 28 11:22:04 2018 +0200
     1.3 @@ -200,10 +200,8 @@
     1.4          |> Config.put_generic ML_Env.ML_write_global true
     1.5          |> ML_Context.exec (fn () =>
     1.6              ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source)
     1.7 -        |> Config.put_generic ML_Env.ML_write_global
     1.8 -            (Config.get_generic context ML_Env.ML_write_global)
     1.9 -        |> Config.put_generic ML_Env.ML_environment
    1.10 -            (Config.get_generic context ML_Env.ML_environment)
    1.11 +        |> Config.restore_generic ML_Env.ML_write_global context
    1.12 +        |> Config.restore_generic ML_Env.ML_environment context
    1.13          |> Local_Theory.propagate_ml_env)));
    1.14  
    1.15  val _ =