interpretation must always operate on the last element in a local theory stack, not on all elements: interpretated facts must disappear after pop from local theory stack, and transfer from last target is not enough
authorhaftmann
Wed May 22 22:56:17 2013 +0200 (2013-05-22)
changeset 5211990ba620333d0
parent 52118 2a976115c7c3
child 52120 e6433b34364b
interpretation must always operate on the last element in a local theory stack, not on all elements: interpretated facts must disappear after pop from local theory stack, and transfer from last target is not enough
src/Pure/Isar/expression.ML
src/Pure/Isar/local_theory.ML
     1.1 --- a/src/Pure/Isar/expression.ML	Wed May 22 22:56:17 2013 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Wed May 22 22:56:17 2013 +0200
     1.3 @@ -855,7 +855,7 @@
     1.4    in setup_proof after_qed propss eqns goal_ctxt end;
     1.5  
     1.6  val activate_proof = Context.proof_map ooo Locale.add_registration;
     1.7 -val activate_local_theory = Local_Theory.target ooo activate_proof;
     1.8 +val activate_local_theory = Local_Theory.surface_target ooo activate_proof;
     1.9  val add_registration = Local_Theory.raw_theory o Context.theory_map ooo Locale.add_registration;
    1.10  fun add_dependency locale dep_morph mixin export =
    1.11    (Local_Theory.raw_theory ooo Locale.add_dependency locale) dep_morph mixin export
     2.1 --- a/src/Pure/Isar/local_theory.ML	Wed May 22 22:56:17 2013 +0200
     2.2 +++ b/src/Pure/Isar/local_theory.ML	Wed May 22 22:56:17 2013 +0200
     2.3 @@ -36,6 +36,7 @@
     2.4    val target_of: local_theory -> Proof.context
     2.5    val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
     2.6    val target_morphism: local_theory -> morphism
     2.7 +  val surface_target: (Proof.context -> Proof.context) -> local_theory -> local_theory
     2.8    val propagate_ml_env: generic_theory -> generic_theory
     2.9    val operations_of: local_theory -> operations
    2.10    val define: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
    2.11 @@ -231,6 +232,10 @@
    2.12  
    2.13  fun target_morphism lthy = standard_morphism lthy (target_of lthy);
    2.14  
    2.15 +fun surface_target f =
    2.16 +  map_first_lthy (fn (naming, operations, after_close, brittle, target) =>
    2.17 +    (naming, operations, after_close, brittle, f target));
    2.18 +
    2.19  fun propagate_ml_env (context as Context.Proof lthy) =
    2.20        let val inherit = ML_Env.inherit context in
    2.21          lthy