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;