--- 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
--- 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 ();