| changeset 71553 | cf2406e654cf |
| parent 71530 | 046cf49162a3 |
| child 71777 | 3875815f5967 |
--- 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))