diff -r f9fd15d3cfac -r c82f59c47aaf src/Pure/morphism.ML
--- a/src/Pure/morphism.ML	Mon Jun 03 17:01:28 2019 +0200
+++ b/src/Pure/morphism.ML	Mon Jun 03 20:09:43 2019 +0200
@@ -125,7 +125,7 @@
 fun fact_morphism a fact = morphism a {binding = [], typ = [], term = [], fact = [fact]};
 fun thm_morphism a thm = morphism a {binding = [], typ = [], term = [], fact = [map thm]};
 
-val transfer_morphism = thm_morphism "transfer" o Thm.transfer;
+val transfer_morphism = thm_morphism "transfer" o Thm.join_transfer;
 val transfer_morphism' = transfer_morphism o Proof_Context.theory_of;
 val transfer_morphism'' = transfer_morphism o Context.theory_of;