# HG changeset patch
# User wenzelm
# Date 1572622577 -3600
# Node ID 71d1971d67adca163751db51a12e72d1b16020ea
# Parent  a802d42c00bc06cddcfbb7f445b0013af6a04faa
make double-sure that internal proof boxes are exported, e.g. in Pure;

diff -r a802d42c00bc -r 71d1971d67ad src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Fri Nov 01 15:47:31 2019 +0100
+++ b/src/Pure/proofterm.ML	Fri Nov 01 16:36:17 2019 +0100
@@ -2095,14 +2095,15 @@
       | export_boxes (Abst (_, _, prf)) = export_boxes prf
       | export_boxes (prf1 %% prf2) = export_boxes prf1 #> export_boxes prf2
       | export_boxes (prf % _) = export_boxes prf
-      | export_boxes (PThm ({serial = i, name = "", ...}, thm_body)) =
+      | export_boxes (PThm ({serial = i, ...}, thm_body)) =
           (fn boxes =>
             if Inttab.defined boxes i then boxes
             else
               let
-                val prf = thm_body_proof_raw thm_body;
-                val boxes' = Inttab.update (i, thm_body_export_proof thm_body) boxes;
-              in export_boxes prf boxes' end)
+                val prf' = thm_body_proof_raw thm_body;
+                val export = thm_body_export_proof thm_body;
+                val boxes' = boxes |> not (Lazy.is_finished export) ? Inttab.update (i, export);
+              in export_boxes prf' boxes' end)
       | export_boxes _ = I;
     val boxes = (proof, Inttab.empty) |-> export_boxes |> Inttab.dest;
   in List.app (Lazy.force o #2) boxes end;