src/Pure/Isar/local_theory.ML
changeset 68865 dd44e31ca2c6
parent 68851 6c9825c1e26b
child 69058 f4fb93197670
     1.1 --- a/src/Pure/Isar/local_theory.ML	Fri Aug 31 16:17:30 2018 +0200
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Fri Aug 31 22:25:58 2018 +0200
     1.3 @@ -251,7 +251,7 @@
     1.4  fun target_morphism lthy = standard_morphism lthy (target_of lthy);
     1.5  
     1.6  fun propagate_ml_env (context as Context.Proof lthy) =
     1.7 -      let val inherit = ML_Env.inherit context in
     1.8 +      let val inherit = ML_Env.inherit [context] in
     1.9          lthy
    1.10          |> background_theory (Context.theory_map inherit)
    1.11          |> map_contexts (K (Context.proof_map inherit))