# HG changeset patch
# User wenzelm
# Date 1572627207 -3600
# Node ID 52a62342c9ce85e4f48ffe615c6516e214380464
# Parent  71d1971d67adca163751db51a12e72d1b16020ea
clarified signature;

diff -r 71d1971d67ad -r 52a62342c9ce src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Fri Nov 01 16:36:17 2019 +0100
+++ b/src/Pure/Thy/export_theory.ML	Fri Nov 01 17:53:27 2019 +0100
@@ -248,8 +248,6 @@
 
     (* theorems and proof terms *)
 
-    val export_standard_proofs = Options.default_bool @{system_option export_standard_proofs};
-
     val clean_thm = Thm.check_hyps (Context.Theory thy) #> Thm.strip_shyps;
 
     val lookup_thm_id = Global_Theory.lookup_thm_id thy;
@@ -285,16 +283,13 @@
         val boxes = proof_boxes thm thm_id;
 
         val proof0 =
-          if export_standard_proofs then
+          if Proofterm.export_standard_enabled () then
             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 Context.theory_name thy = Context.PureN orelse
-            (not export_standard_proofs andalso Proofterm.export_enabled ())
-          then Proofterm.commit_proof proof else ();
+        val _ = Proofterm.commit_proof thy proof;
       in
         (prop, (deps, (boxes, proof))) |>
           let
diff -r 71d1971d67ad -r 52a62342c9ce src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Fri Nov 01 16:36:17 2019 +0100
+++ b/src/Pure/proofterm.ML	Fri Nov 01 17:53:27 2019 +0100
@@ -173,8 +173,9 @@
   val add_standard_vars_term: term -> (string * typ) list -> (string * typ) list
 
   val export_enabled: unit -> bool
+  val export_standard_enabled: unit -> bool
   val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
-  val commit_proof: proof -> unit
+  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
@@ -2088,8 +2089,9 @@
 (* PThm nodes *)
 
 fun export_enabled () = Options.default_bool "export_proofs";
+fun export_standard_enabled () = Options.default_bool "export_standard_proofs";
 
-fun commit_proof proof =
+fun export_proof_boxes proof =
   let
     fun export_boxes (AbsP (_, _, prf)) = export_boxes prf
       | export_boxes (Abst (_, _, prf)) = export_boxes prf
@@ -2108,6 +2110,11 @@
     val boxes = (proof, Inttab.empty) |-> 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) =
@@ -2156,7 +2163,7 @@
 fun export thy i prop prf =
   if export_enabled () then
     let
-      val _ = commit_proof prf;
+      val _ = export_proof_boxes prf;
       val _ = export_proof thy i prop prf;
     in () end
   else ();