src/Pure/proofterm.ML

   val standard_vars_term: Name.context -> term -> term
   val add_standard_vars: proof -> (string * typ) list -> (string * typ) list
   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
   val unconstrain_thm_proof: theory -> (class * class -> proof) ->
     (string * class list list * class -> proof) -> sort list -> term ->

 
 
 (* PThm nodes *)
 
 fun export_enabled () = Options.default_bool "export_proofs";
-
-fun commit_proof proof =
+fun export_standard_enabled () = Options.default_bool "export_standard_proofs";
+
+fun export_proof_boxes proof =
   let
     fun export_boxes (AbsP (_, _, prf)) = export_boxes prf
       | export_boxes (Abst (_, _, prf)) = export_boxes prf
       | export_boxes (prf1 %% prf2) = export_boxes prf1 #> export_boxes prf2
       | export_boxes (prf % _) = export_boxes prf

                 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;
   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) =
   let

   end;
 
 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 ();
 
 fun prune proof =