diff -r 56f96489478c -r 9c19e15c8548 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Mon Jun 03 23:29:05 2019 +0200
+++ b/src/Pure/thm.ML	Mon Jun 03 23:58:20 2019 +0200
@@ -90,6 +90,7 @@
   val transfer': Proof.context -> thm -> thm
   val transfer'': Context.generic -> thm -> thm
   val join_transfer: theory -> thm -> thm
+  val join_transfer_context: Proof.context * thm -> Proof.context * thm
   val renamed_prop: term -> thm -> thm
   val weaken: cterm -> thm -> thm
   val weaken_sorts: sort list -> cterm -> cterm
@@ -535,6 +536,11 @@
   if Context.subthy_id (Context.theory_id thy, theory_id th) then th
   else transfer thy th;
 
+fun join_transfer_context (ctxt, th) =
+  if Context.subthy_id (Context.theory_id (Proof_Context.theory_of ctxt), theory_id th) then
+    (Context.raw_transfer (theory_of_thm th) ctxt, th)
+  else (ctxt, transfer' ctxt th);
+
 
 (* matching *)