# HG changeset patch
# User wenzelm
# Date 1572628126 -3600
# Node ID 5e98925f86ede3a9bc68bf0d74a4b9455623c5b0
# Parent  52a62342c9ce85e4f48ffe615c6516e214380464
clarified signature (again);

diff -r 52a62342c9ce -r 5e98925f86ed src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Fri Nov 01 17:53:27 2019 +0100
+++ b/src/Pure/Thy/export_theory.ML	Fri Nov 01 18:08:46 2019 +0100
@@ -289,7 +289,9 @@
           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
diff -r 52a62342c9ce -r 5e98925f86ed src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Fri Nov 01 17:53:27 2019 +0100
+++ b/src/Pure/proofterm.ML	Fri Nov 01 18:08:46 2019 +0100
@@ -174,8 +174,9 @@
 
   val export_enabled: unit -> bool
   val export_standard_enabled: unit -> bool
+  val export_proof_boxes_required: theory -> bool
+  val export_proof_boxes: proof list -> unit
   val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
-  val commit_proof: theory -> proof -> unit
   val thm_proof: theory -> (class * class -> proof) ->
     (string * class list list * class -> proof) -> string * Position.T -> sort list ->
     term list -> term -> (serial * proof_body future) list -> proof_body -> thm * proof
@@ -2091,7 +2092,11 @@
 fun export_enabled () = Options.default_bool "export_proofs";
 fun export_standard_enabled () = Options.default_bool "export_standard_proofs";
 
-fun export_proof_boxes proof =
+fun export_proof_boxes_required thy =
+  Context.theory_name thy = Context.PureN orelse
+    (export_enabled () andalso not (export_standard_enabled ()));
+
+fun export_proof_boxes proofs =
   let
     fun export_boxes (AbsP (_, _, prf)) = export_boxes prf
       | export_boxes (Abst (_, _, prf)) = export_boxes prf
@@ -2107,14 +2112,9 @@
                 val boxes' = boxes |> not (Lazy.is_finished export) ? Inttab.update (i, export);
               in export_boxes prf' boxes' end)
       | export_boxes _ = I;
-    val boxes = (proof, Inttab.empty) |-> export_boxes |> Inttab.dest;
+    val boxes = (proofs, Inttab.empty) |-> fold export_boxes |> Inttab.dest;
   in List.app (Lazy.force o #2) boxes end;
 
-fun commit_proof thy proof =
-  if Context.theory_name thy = Context.PureN orelse
-    (export_enabled () andalso not (export_standard_enabled ()))
-  then export_proof_boxes proof else ();
-
 local
 
 fun unconstrainT_proof algebra classrel_proof arity_proof (ucontext: Logic.unconstrain_context) =
@@ -2163,7 +2163,7 @@
 fun export thy i prop prf =
   if export_enabled () then
     let
-      val _ = export_proof_boxes prf;
+      val _ = export_proof_boxes [prf];
       val _ = export_proof thy i prop prf;
     in () end
   else ();