# HG changeset patch
# User wenzelm
# Date 1575057148 -3600
# Node ID c7d4f2ab40b9adfb05eb7c029c0372dab0a4fb75
# Parent  71467e35fc3ca64ab6e25cd3fb443a7f1907c470
proper theory context, e.g. for Thm.transfer;

diff -r 71467e35fc3c -r c7d4f2ab40b9 src/Pure/Isar/generic_target.ML
--- 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 =