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 _ =
-          if Proofterm.export_proof_boxes_required thy
-          then Proofterm.export_proof_boxes [proof] else ();
+        val _ = Thm.expose_proofs thy [thm];
       in
         (prop, deps, proof) |>
           let
             open XML.Encode Term_XML.Encode;
             val encode_proof = Proofterm.encode_standard_proof consts;