src/Pure/thm.ML
changeset 71177 71467e35fc3c
parent 71088 4b45d592ce29
child 71447 439410bf4519
--- a/src/Pure/thm.ML	Tue Nov 26 14:32:08 2019 +0000
+++ b/src/Pure/thm.ML	Thu Nov 28 18:13:23 2019 +0100
@@ -610,9 +610,9 @@
   else transfer thy th;
 
 fun join_transfer_context (ctxt, th) =
-  if Context.subthy_id (Context.theory_id (Proof_Context.theory_of ctxt), theory_id th) then
-    (Context.raw_transfer (theory_of_thm th) ctxt, th)
-  else (ctxt, transfer' ctxt th);
+  if Context.subthy_id (theory_id th, Context.theory_id (Proof_Context.theory_of ctxt))
+  then (ctxt, transfer' ctxt th)
+  else (Context.raw_transfer (theory_of_thm th) ctxt, th);
 
 
 (* matching *)