# HG changeset patch
# User wenzelm
# Date 1684152838 -7200
# Node ID f16067da45ef7dab610db6e1ad48595c4126dffe
# Parent  d7395ef8129282516da9eab9450425a41b494d0f
avoid capture of inner/outer context and thus reduce heaps sizes by 20..40% (see also dd04a8b654fc, e49bf4ebf330, 9c19e15c8548, 71467e35fc3c);

diff -r d7395ef81292 -r f16067da45ef src/Pure/Isar/proof_context.ML
--- 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;
 
 
 
diff -r d7395ef81292 -r f16067da45ef src/Pure/assumption.ML
--- 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;
diff -r d7395ef81292 -r f16067da45ef src/Pure/variable.ML
--- 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;