# HG changeset patch
# User wenzelm
# Date 1584219509 -3600
# Node ID cf2406e654cf65e4a712c4fd5a650eb7f2894596
# Parent  309eeea0b2c6e5e80de4f388fa88419185cc8943
more robust: proper transfer if Context.eq_thy_id;

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))