# HG changeset patch
# User wenzelm
# Date 1559599100 -7200
# Node ID 9c19e15c854814faf3bff6ec1ad125bd9ce3a2f1
# Parent  56f96489478c887db78b8a5727b4a0ece3f5acdd
more structural integrity;

diff -r 56f96489478c -r 9c19e15c8548 src/Pure/assumption.ML
--- a/src/Pure/assumption.ML	Mon Jun 03 23:29:05 2019 +0200
+++ b/src/Pure/assumption.ML	Mon Jun 03 23:58:20 2019 +0200
@@ -108,10 +108,14 @@
 
 (* export *)
 
+fun normalize ctxt0 th0 =
+  let val (ctxt, th) = Thm.join_transfer_context (ctxt0, th0)
+  in Raw_Simplifier.norm_hhf_protect ctxt th end;
+
 fun export is_goal inner outer =
-  Raw_Simplifier.norm_hhf_protect inner #>
+  normalize inner #>
   fold_rev (fn (e, As) => #1 (e is_goal As)) (local_assumptions_of inner outer) #>
-  Raw_Simplifier.norm_hhf_protect outer;
+  normalize outer;
 
 fun export_term inner outer =
   fold_rev (fn (e, As) => #2 (e false As)) (local_assumptions_of inner outer);
@@ -122,6 +126,8 @@
     val term = export_term inner outer;
     val typ = Logic.type_map term;
   in
+    Morphism.transfer_morphism' inner $>
+    Morphism.transfer_morphism' outer $>
     Morphism.morphism "Assumption.export"
       {binding = [], typ = [typ], term = [term], fact = [map thm]}
   end;
diff -r 56f96489478c -r 9c19e15c8548 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Mon Jun 03 23:29:05 2019 +0200
+++ b/src/Pure/thm.ML	Mon Jun 03 23:58:20 2019 +0200
@@ -90,6 +90,7 @@
   val transfer': Proof.context -> thm -> thm
   val transfer'': Context.generic -> thm -> thm
   val join_transfer: theory -> thm -> thm
+  val join_transfer_context: Proof.context * thm -> Proof.context * thm
   val renamed_prop: term -> thm -> thm
   val weaken: cterm -> thm -> thm
   val weaken_sorts: sort list -> cterm -> cterm
@@ -535,6 +536,11 @@
   if Context.subthy_id (Context.theory_id thy, theory_id th) then th
   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);
+
 
 (* matching *)