added inherit_env;

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