diff -r 309eeea0b2c6 -r cf2406e654cf src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Mar 14 20:36:16 2020 +0100
+++ b/src/Pure/thm.ML	Sat Mar 14 21:58:29 2020 +0100
@@ -606,8 +606,7 @@
 val transfer'' = transfer o Context.theory_of;
 
 fun join_transfer thy th =
-  if Context.subthy_id (Context.theory_id thy, theory_id th) then th
-  else transfer thy th;
+  (Context.subthy_id (theory_id th, Context.theory_id thy) ? transfer thy) th;
 
 fun join_transfer_context (ctxt, th) =
   if Context.subthy_id (theory_id th, Context.theory_id (Proof_Context.theory_of ctxt))