--- a/src/Pure/thm.ML Sun Nov 03 15:45:46 2019 +0100
+++ b/src/Pure/thm.ML Sun Nov 03 15:48:59 2019 +0100
@@ -102,6 +102,7 @@
val proof_body_of: thm -> proof_body
val proof_of: thm -> proof
val consolidate: thm list -> unit
+ val expose_proofs: theory -> thm list -> unit
val future: thm future -> cterm -> thm
val thm_deps: thm -> Proofterm.thm Ord_List.T
val derivation_closed: thm -> bool
@@ -760,6 +761,11 @@
val consolidate = ignore o proof_bodies_of;
+fun expose_proofs thy thms =
+ if Proofterm.export_proof_boxes_required thy then
+ Proofterm.export_proof_boxes (map proof_of thms)
+ else ();
+
(* future rule *)