clarified transfer_morphism: implicit join_certificate, e.g. relevant for complex cascades of morphisms such as class locale interpretation;

--- 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;
 

--- a/src/Pure/thm.ML	Mon Jun 03 17:01:28 2019 +0200
+++ b/src/Pure/thm.ML	Mon Jun 03 20:09:43 2019 +0200
@@ -89,6 +89,7 @@
   val transfer: theory -> thm -> thm
   val transfer': Proof.context -> thm -> thm
   val transfer'': Context.generic -> thm -> thm
+  val join_transfer: theory -> thm -> thm
   val renamed_prop: term -> thm -> thm
   val weaken: cterm -> thm -> thm
   val weaken_sorts: sort list -> cterm -> cterm
@@ -530,6 +531,10 @@
 val transfer' = transfer o Proof_Context.theory_of;
 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;
+
 
 (* matching *)