src/Pure/Isar/local_theory.ML
changeset 37949 48a874444164
parent 36610 bafd82950e24
child 38308 0e4649095739
     1.1 --- a/src/Pure/Isar/local_theory.ML	Fri Jul 23 18:42:46 2010 +0200
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Sat Jul 24 12:14:53 2010 +0200
     1.3 @@ -5,6 +5,7 @@
     1.4  *)
     1.5  
     1.6  type local_theory = Proof.context;
     1.7 +type generic_theory = Context.generic;
     1.8  
     1.9  signature LOCAL_THEORY =
    1.10  sig
    1.11 @@ -25,6 +26,7 @@
    1.12    val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory
    1.13    val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
    1.14    val map_contexts: (Context.generic -> Context.generic) -> local_theory -> local_theory
    1.15 +  val propagate_ml_env: generic_theory -> generic_theory
    1.16    val standard_morphism: local_theory -> Proof.context -> morphism
    1.17    val target_morphism: local_theory -> morphism
    1.18    val global_morphism: local_theory -> morphism
    1.19 @@ -173,6 +175,10 @@
    1.20    target (Context.proof_map f) #>
    1.21    Context.proof_map f;
    1.22  
    1.23 +fun propagate_ml_env (context as Context.Proof lthy) =
    1.24 +      Context.Proof (map_contexts (ML_Env.inherit context) lthy)
    1.25 +  | propagate_ml_env context = context;
    1.26 +
    1.27  
    1.28  (* morphisms *)
    1.29