support multiple inheritance of ML environments, with canonical merge order as in Context.begin_theory;

--- a/src/Pure/Isar/local_theory.ML	Fri Aug 31 16:17:30 2018 +0200
+++ b/src/Pure/Isar/local_theory.ML	Fri Aug 31 22:25:58 2018 +0200
@@ -251,7 +251,7 @@
 fun target_morphism lthy = standard_morphism lthy (target_of lthy);
 
 fun propagate_ml_env (context as Context.Proof lthy) =
-      let val inherit = ML_Env.inherit context in
+      let val inherit = ML_Env.inherit [context] in
         lthy
         |> background_theory (Context.theory_map inherit)
         |> map_contexts (K (Context.proof_map inherit))

--- a/src/Pure/Isar/proof.ML	Fri Aug 31 16:17:30 2018 +0200
+++ b/src/Pure/Isar/proof.ML	Fri Aug 31 22:25:58 2018 +0200
@@ -237,7 +237,7 @@
 fun map_contexts f = map_all (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
 
 fun propagate_ml_env state = map_contexts
-  (Context.proof_map (ML_Env.inherit (Context.Proof (context_of state)))) state;
+  (Context.proof_map (ML_Env.inherit [Context.Proof (context_of state)])) state;
 
 
 (* facts *)

--- a/src/Pure/ML/ml_context.ML	Fri Aug 31 16:17:30 2018 +0200
+++ b/src/Pure/ML/ml_context.ML	Fri Aug 31 22:25:58 2018 +0200
@@ -168,7 +168,7 @@
         (Option.map (Context.Proof o Context_Position.set_visible false) env_ctxt)
         (fn () =>
           (ML_Compiler.eval non_verbose Position.none env; Context.get_generic_context ())) ()
-      |> (fn NONE => () | SOME context' => Context.>> (ML_Env.inherit context'));
+      |> (fn NONE => () | SOME context' => Context.>> (ML_Env.inherit [context']));
 
     (*eval body*)
     val _ = ML_Compiler.eval flags pos body;

--- a/src/Pure/ML/ml_env.ML	Fri Aug 31 16:17:30 2018 +0200
+++ b/src/Pure/ML/ml_env.ML	Fri Aug 31 22:25:58 2018 +0200
@@ -15,7 +15,7 @@
   val ML_read_global: bool Config.T
   val ML_write_global_raw: Config.raw
   val ML_write_global: bool Config.T
-  val inherit: Context.generic -> Context.generic -> Context.generic
+  val inherit: Context.generic list -> Context.generic -> Context.generic
   type operations =
    {read_source: Input.source -> ML_Lex.token Antiquote.antiquote list,
     explode_token: ML_Lex.token -> char list}
@@ -101,20 +101,31 @@
  {read_source: Input.source -> ML_Lex.token Antiquote.antiquote list,
   explode_token: ML_Lex.token -> char list};
 
+local
+
 type env = tables * operations;
+type data = env Name_Space.table * (bool Unsynchronized.ref * Position.T) Inttab.table;
+
+val empty_data: data = (Name_Space.empty_table "ML_environment", Inttab.empty);
+
+fun merge_data ((envs1, breakpoints1), (envs2, breakpoints2)) : data =
+  ((envs1, envs2) |> Name_Space.join_tables
+    (K (fn ((tables1, ops), (tables2, _)) => (merge_tables (tables1, tables2), ops))),
+   Inttab.merge (K true) (breakpoints1, breakpoints2));
+
+in
 
 structure Data = Generic_Data
 (
-  type T = env Name_Space.table * (bool Unsynchronized.ref * Position.T) Inttab.table;
-  val empty: T = (Name_Space.empty_table "ML_environment", Inttab.empty);
+  type T = data;
+  val empty = empty_data;
   val extend = I;
-  fun merge ((envs1, breakpoints1), (envs2, breakpoints2)) : T =
-    ((envs1, envs2) |> Name_Space.join_tables
-      (K (fn ((tables1, ops), (tables2, _)) => (merge_tables (tables1, tables2), ops))),
-     Inttab.merge (K true) (breakpoints1, breakpoints2));
+  val merge = merge_data;
 );
 
-val inherit = Data.put o Data.get;
+fun inherit contexts = Data.put (Library.foldl1 merge_data (map Data.get contexts));
+
+end;
 
 val get_env = Name_Space.get o #1 o Data.get;
 val get_tables = #1 oo get_env;