src/Pure/Isar/local_theory.ML

--- 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))