avoid capture of inner/outer context and thus reduce heaps sizes by 20..40% (see also dd04a8b654fc, e49bf4ebf330, 9c19e15c8548, 71467e35fc3c);

--- a/src/Pure/Isar/proof_context.ML	Mon May 15 14:10:44 2023 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon May 15 14:13:58 2023 +0200
@@ -852,7 +852,7 @@
 
 fun norm_export_morphism inner outer =
   export_morphism inner outer $>
-  Morphism.thm_morphism "Proof_Context.norm_export" (Goal.norm_result outer);
+  Morphism.thm_morphism "Proof_Context.norm_export" Goal.norm_result_without_context;
 
 
 

--- a/src/Pure/assumption.ML	Mon May 15 14:10:44 2023 +0200
+++ b/src/Pure/assumption.ML	Mon May 15 14:13:58 2023 +0200
@@ -129,9 +129,9 @@
 (* export *)
 
 fun export is_goal inner outer =
-  Raw_Simplifier.norm_hhf_protect inner #>
+  Raw_Simplifier.norm_hhf_protect_without_context #>
   fold_rev (fn (e, As) => #1 (e is_goal As)) (local_assumptions_of inner outer) #>
-  Raw_Simplifier.norm_hhf_protect outer;
+  Raw_Simplifier.norm_hhf_protect_without_context;
 
 fun export_term inner outer =
   fold_rev (fn (e, As) => #2 (e false As)) (local_assumptions_of inner outer);
@@ -142,8 +142,6 @@
     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/variable.ML	Mon May 15 14:10:44 2023 +0200
+++ b/src/Pure/variable.ML	Mon May 15 14:13:58 2023 +0200
@@ -583,8 +583,6 @@
     val term = singleton (export_terms inner outer);
     val typ = Logic.type_map term;
   in
-    Morphism.transfer_morphism' inner $>
-    Morphism.transfer_morphism' outer $>
     Morphism.morphism "Variable.export" {binding = [], typ = [typ], term = [term], fact = [fact]}
   end;