src/Pure/proofterm.ML

   Future.joins (map (thm_node_body o #2) thms);
 
 val consolidate_bodies =
   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 =
       Lazy.lazy_name "Proofterm.make_thm_node" (fn () =>

 fun fulfill_proof_future thy promises (postproc: proof_body -> proof_body) body =
   let
     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
       (singleton o Future.forks)
         {name = "Proofterm.fulfill_proof_future", group = NONE,