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