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