more compact: avoid pointless PThm rudiments;

--- a/src/Pure/Thy/export_theory.ML	Fri Aug 23 13:20:13 2019 +0200
+++ b/src/Pure/Thy/export_theory.ML	Fri Aug 23 13:32:27 2019 +0200
@@ -261,11 +261,10 @@
       let
         val deps = map (Thm_Name.print o #2) (Thm_Deps.thm_deps thy raw_thm);
         val thm = clean_thm raw_thm;
+        val raw_proof =
+          if Proofterm.export_enabled () then Thm.reconstruct_proof_of thm else Proofterm.MinProof;
         val (prop, proof) =
-          standard_prop Name.context
-            (Thm.extra_shyps thm)
-            (Thm.full_prop_of thm)
-            (try Thm.reconstruct_proof_of thm);
+          standard_prop Name.context (Thm.extra_shyps thm) (Thm.full_prop_of thm) (SOME raw_proof);
       in
         (prop, (deps, proof)) |>
           let open XML.Encode Term_XML.Encode

--- a/src/Pure/proofterm.ML	Fri Aug 23 13:20:13 2019 +0200
+++ b/src/Pure/proofterm.ML	Fri Aug 23 13:32:27 2019 +0200
@@ -163,6 +163,7 @@
   val standard_vars: Name.context -> term * proof option -> term * proof option
   val standard_vars_term: Name.context -> term -> term
 
+  val export_enabled: unit -> bool
   val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
   val thm_proof: theory -> (class * class -> proof) ->
     (string * class list list * class -> proof) -> string * Position.T -> sort list ->
@@ -2042,6 +2043,8 @@
 
 (* PThm nodes *)
 
+fun export_enabled () = Options.default_bool "export_proofs";
+
 local
 
 fun unconstrainT_proof algebra classrel_proof arity_proof (ucontext: Logic.unconstrain_context) =
@@ -2099,8 +2102,6 @@
     val boxes = (proof, Inttab.empty) |-> export_boxes |> Inttab.dest;
   in List.app (Lazy.force o #2) boxes end;
 
-fun export_enabled () = Options.default_bool "export_proofs";
-
 fun export thy i prop prf =
   if export_enabled () then (export_proof_boxes prf; export_proof thy i prop prf) else ();