# HG changeset patch
# User wenzelm
# Date 1629296020 -7200
# Node ID 0faa68dedce54674db8d3ae64d6208ea5c6d6163
# Parent  62b0577123a57f52ac43fcb8d86441b9fde0e255
consolidate_body more thoroughly, e.g. for reduced ML_Heap.obj_size;

diff -r 62b0577123a5 -r 0faa68dedce5 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Mon Aug 16 23:07:01 2021 +0200
+++ b/src/Pure/proofterm.ML	Wed Aug 18 16:13:40 2021 +0200
@@ -266,6 +266,8 @@
   maps (fn PBody {thms, ...} => map (thm_node_consolidate o #2) thms)
   #> Lazy.consolidate #> map Lazy.force #> ignore;
 
+val consolidate_body = consolidate_bodies o single;
+
 fun make_thm_node theory_name name prop body export =
   let
     val consolidate =
@@ -1981,7 +1983,7 @@
     fun fulfill () =
       postproc (fulfill_norm_proof thy (map (apsnd Future.join) promises) (Future.join body));
   in
-    if null promises then Future.map postproc body
+    if null promises then Future.map (postproc #> tap consolidate_body) body
     else if Future.is_finished body andalso length promises = 1 then
       Future.map (fn _ => fulfill ()) (snd (hd promises))
     else