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

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

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