tuned;

--- a/src/Pure/Isar/attrib.ML	Thu Aug 14 11:55:09 2014 +0200
+++ b/src/Pure/Isar/attrib.ML	Thu Aug 14 12:13:24 2014 +0200
@@ -102,10 +102,10 @@
 
 val get_attributes = Attributes.get o Context.Proof;
 
-fun transfer_attributes thy ctxt =
+fun transfer_attributes ctxt =
   let
-    val attribs' =
-      Name_Space.merge_tables (Attributes.get (Context.Theory thy), get_attributes ctxt);
+    val attribs0 = Attributes.get (Context.Theory (Proof_Context.theory_of ctxt));
+    val attribs' = Name_Space.merge_tables (attribs0, get_attributes ctxt);
   in Context.proof_map (Attributes.put attribs') ctxt end;
 
 fun print_attributes ctxt =
@@ -133,16 +133,11 @@
   in (name, Context.the_theory (Attributes.put attribs' context)) end;
 
 fun define binding att comment lthy =
-  let
-    val standard_morphism =
-      Local_Theory.standard_morphism lthy (Proof_Context.init_global (Proof_Context.theory_of lthy));
-    val att0 = att o Args.transform_values standard_morphism;
-  in
+  let val att0 = att o Args.transform_values (Local_Theory.background_morphism lthy) in
     lthy
     |> Local_Theory.background_theory_result (define_global binding att0 comment)
     |-> (fn name =>
-      Local_Theory.map_contexts
-        (fn _ => fn ctxt => transfer_attributes (Proof_Context.theory_of ctxt) ctxt)
+      Local_Theory.map_contexts (K transfer_attributes)
       #> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context =>
           let
             val naming = Name_Space.naming_of context;

--- a/src/Pure/Isar/local_theory.ML	Thu Aug 14 11:55:09 2014 +0200
+++ b/src/Pure/Isar/local_theory.ML	Thu Aug 14 12:13:24 2014 +0200
@@ -39,6 +39,7 @@
   val raw_theory: (theory -> theory) -> local_theory -> local_theory
   val background_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
   val background_theory: (theory -> theory) -> local_theory -> local_theory
+  val background_morphism: local_theory -> morphism
   val target_of: local_theory -> Proof.context
   val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
   val target_morphism: local_theory -> morphism
@@ -222,6 +223,9 @@
 
 fun background_theory f = #2 o background_theory_result (f #> pair ());
 
+fun background_morphism lthy =
+  standard_morphism lthy (Proof_Context.init_global (Proof_Context.theory_of lthy));
+
 
 (* target contexts *)
 

--- a/src/Pure/Isar/method.ML	Thu Aug 14 11:55:09 2014 +0200
+++ b/src/Pure/Isar/method.ML	Thu Aug 14 12:13:24 2014 +0200
@@ -322,10 +322,10 @@
 
 val get_methods = Methods.get o Context.Proof;
 
-fun transfer_methods thy ctxt =
+fun transfer_methods ctxt =
   let
-    val meths' =
-      Name_Space.merge_tables (Methods.get (Context.Theory thy), get_methods ctxt);
+    val meths0 = Methods.get (Context.Theory (Proof_Context.theory_of ctxt));
+    val meths' = Name_Space.merge_tables (meths0, get_methods ctxt);
   in Context.proof_map (Methods.put meths') ctxt end;
 
 fun print_methods ctxt =
@@ -351,16 +351,11 @@
   in (name, Context.the_theory (Methods.put meths' context)) end;
 
 fun define binding meth comment lthy =
-  let
-    val standard_morphism =
-      Local_Theory.standard_morphism lthy (Proof_Context.init_global (Proof_Context.theory_of lthy));
-    val meth0 = meth o Args.transform_values standard_morphism;
-  in
+  let val meth0 = meth o Args.transform_values (Local_Theory.background_morphism lthy) in
     lthy
     |> Local_Theory.background_theory_result (define_global binding meth0 comment)
     |-> (fn name =>
-      Local_Theory.map_contexts
-        (fn _ => fn ctxt => transfer_methods (Proof_Context.theory_of ctxt) ctxt)
+      Local_Theory.map_contexts (K transfer_methods)
       #> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context =>
           let
             val naming = Name_Space.naming_of context;