# HG changeset patch
# User wenzelm
# Date 1221682019 -7200
# Node ID 7d56de7e2305623ab4840350737dabe6d0962dc0
# Parent  7af26c1f02eca2f43eaf5134d2ea4b7949587549
added inherit_env;

diff -r 7af26c1f02ec -r 7d56de7e2305 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Wed Sep 17 22:06:57 2008 +0200
+++ b/src/Pure/ML/ml_context.ML	Wed Sep 17 22:06:59 2008 +0200
@@ -20,6 +20,7 @@
   val the_global_context: unit -> theory
   val the_local_context: unit -> Proof.context
   val exec: (unit -> unit) -> Context.generic -> Context.generic
+  val inherit_env: Proof.context -> Proof.context -> Proof.context
   val name_space: ML_NameSpace.nameSpace
   val stored_thms: thm list ref
   val ml_store_thm: string * thm -> unit
@@ -78,6 +79,8 @@
     Symtab.merge (K true) (functor1, functor2));
 );
 
+val inherit_env = Context.proof_map o ML_Env.put o ML_Env.get o Context.Proof;
+
 val name_space: ML_NameSpace.nameSpace =
   let
     fun lookup sel1 sel2 name =