# HG changeset patch # User haftmann # Date 1369256177 -7200 # Node ID 90ba620333d00a0420ee484bdd917a9d460b2cad # Parent 2a976115c7c38c783213f826b690b46e608b2b67 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 diff -r 2a976115c7c3 -r 90ba620333d0 src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Wed May 22 22:56:17 2013 +0200 +++ b/src/Pure/Isar/expression.ML Wed May 22 22:56:17 2013 +0200 @@ -855,7 +855,7 @@ in setup_proof after_qed propss eqns goal_ctxt end; val activate_proof = Context.proof_map ooo Locale.add_registration; -val activate_local_theory = Local_Theory.target ooo activate_proof; +val activate_local_theory = Local_Theory.surface_target ooo activate_proof; val add_registration = Local_Theory.raw_theory o Context.theory_map ooo Locale.add_registration; fun add_dependency locale dep_morph mixin export = (Local_Theory.raw_theory ooo Locale.add_dependency locale) dep_morph mixin export diff -r 2a976115c7c3 -r 90ba620333d0 src/Pure/Isar/local_theory.ML --- a/src/Pure/Isar/local_theory.ML Wed May 22 22:56:17 2013 +0200 +++ b/src/Pure/Isar/local_theory.ML Wed May 22 22:56:17 2013 +0200 @@ -36,6 +36,7 @@ val target_of: local_theory -> Proof.context val target: (Proof.context -> Proof.context) -> local_theory -> local_theory val target_morphism: local_theory -> morphism + val surface_target: (Proof.context -> Proof.context) -> local_theory -> local_theory val propagate_ml_env: generic_theory -> generic_theory val operations_of: local_theory -> operations val define: (binding * mixfix) * (Attrib.binding * term) -> local_theory -> @@ -231,6 +232,10 @@ fun target_morphism lthy = standard_morphism lthy (target_of lthy); +fun surface_target f = + map_first_lthy (fn (naming, operations, after_close, brittle, target) => + (naming, operations, after_close, brittle, f target)); + fun propagate_ml_env (context as Context.Proof lthy) = let val inherit = ML_Env.inherit context in lthy