more robust: proper transfer if Context.eq_thy_id;
authorwenzelm
Sat, 14 Mar 2020 21:58:29 +0100
changeset 71767 cf2406e654cf
parent 71766 309eeea0b2c6
child 71768 bb923365f9da
child 71769 2a82462276db
more robust: proper transfer if Context.eq_thy_id;
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))