proper theory context, e.g. for Thm.transfer;
authorwenzelm
Fri, 29 Nov 2019 20:52:28 +0100
changeset 71378 c7d4f2ab40b9
parent 71377 71467e35fc3c
child 71379 592e2afdd50c
proper theory context, e.g. for Thm.transfer;
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 =