proper theory context, e.g. for Thm.transfer;

--- a/src/Pure/Isar/generic_target.ML	Thu Nov 28 18:13:23 2019 +0100
+++ b/src/Pure/Isar/generic_target.ML	Fri Nov 29 20:52:28 2019 +0100
@@ -180,9 +180,9 @@
 
 fun background_declaration decl lthy =
   let
-    val theory_decl =
+    fun theory_decl context =
       Local_Theory.standard_form lthy
-        (Proof_Context.init_global (Proof_Context.theory_of lthy)) decl;
+        (Proof_Context.init_global (Context.theory_of context)) decl context;
   in Local_Theory.background_theory (Context.theory_map theory_decl) lthy end;
 
 fun background_abbrev (b, global_rhs) params =