tuned signature;

--- a/src/Pure/global_theory.ML	Sat Nov 02 20:52:24 2019 +0000
+++ b/src/Pure/global_theory.ML	Sat Nov 02 23:13:15 2019 +0100
@@ -291,10 +291,7 @@
   if Binding.is_empty b then
     let
       val (thms, thy') = app_facts facts thy;
-      val _ =
-        if Proofterm.export_proof_boxes_required thy' then
-          Proofterm.export_proof_boxes (map Thm.proof_of thms)
-        else ();
+      val _ = Thm.expose_proofs thy' thms;
     in register_proofs thms thy' end
   else
     let

--- a/src/Pure/more_thm.ML	Sat Nov 02 20:52:24 2019 +0000
+++ b/src/Pure/more_thm.ML	Sat Nov 02 23:13:15 2019 +0100
@@ -113,6 +113,7 @@
   val tag: string * string -> attribute
   val untag: string -> attribute
   val kind: string -> attribute
+  val expose_proofs: theory -> thm list -> unit
   val reconstruct_proof_of: thm -> Proofterm.proof
   val standard_proof_of: {full: bool, expand_name: Proofterm.thm_header -> string option} ->
     thm -> Proofterm.proof
@@ -654,6 +655,11 @@
 
 (** proof terms **)
 
+fun expose_proofs thy thms =
+  if Proofterm.export_proof_boxes_required thy then
+    Proofterm.export_proof_boxes (map Thm.proof_of thms)
+  else ();
+
 fun reconstruct_proof_of thm =
   Proofterm.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);