Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more robust: proper transfer if Context.eq_thy_id;
authorwenzelm
Sat, 14 Mar 2020 21:58:29 +0100
changeset 71553 cf2406e654cf
parent 71552 309eeea0b2c6
child 71554 2a82462276db
more robust: proper transfer if Context.eq_thy_id;
src/Pure/thm.ML file | annotate | diff | comparison | revisions 
--- 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))
isabelle