src/Pure/Thy/export_theory.ML

             Thm.standard_proof_of {full = true, expand_name = SOME o expand_name thm_id} thm
           else if Proofterm.export_enabled () then Thm.reconstruct_proof_of thm
           else MinProof;
         val (prop, SOME proof) =
           standard_prop Name.context (Thm.extra_shyps thm) (Thm.full_prop_of thm) (SOME proof0);
-        val _ = Proofterm.commit_proof thy proof;
+        val _ =
+          if Proofterm.export_proof_boxes_required thy
+          then Proofterm.export_proof_boxes [proof] else ();
       in
         (prop, (deps, (boxes, proof))) |>
           let
             open XML.Encode Term_XML.Encode;
             fun encode_box {serial, theory_name} = pair int string (serial, theory_name);