# HG changeset patch
# User wenzelm
# Date 1535447613 -7200
# Node ID deefe5837120875116860206805c13b6374007c4
# Parent  8207c67d9ef4c66bb96d3e22972718aa03629292
clarified ML_environment: ML_write_global requires "Isabelle";

diff -r 8207c67d9ef4 -r deefe5837120 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Tue Aug 28 10:58:43 2018 +0200
+++ b/src/Pure/Pure.thy	Tue Aug 28 11:13:33 2018 +0200
@@ -196,11 +196,14 @@
     (Parse.ML_source >> (fn source =>
       Toplevel.generic_theory (fn context =>
         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)
         |> Local_Theory.propagate_ml_env)));
 
 val _ =