# 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