# HG changeset patch
# User wenzelm
# Date 1572724582 -3600
# Node ID 699ff83813c0b17f963d8f2b2a8b10a457b417c5
# Parent  9d0712c748349904df89eb9016a42b21a21d7914
proper graph traversal -- avoid exponential blowup (amending 71d1971d67ad);

diff -r 9d0712c74834 -r 699ff83813c0 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sat Nov 02 18:47:00 2019 +0000
+++ b/src/Pure/proofterm.ML	Sat Nov 02 20:56:22 2019 +0100
@@ -2109,7 +2109,7 @@
               let
                 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);
+                val boxes' = Inttab.update (i, export) boxes;
               in export_boxes prf' boxes' end)
       | export_boxes _ = I;
     val boxes = (proofs, Inttab.empty) |-> fold export_boxes |> Inttab.dest;