# HG changeset patch # User wenzelm # Date 1566559947 -7200 # Node ID 8088cf2576f31bdb6182d171ff0e06494c490639 # Parent 706dac15554ba09674cb7c446cf3f2baebda1630 more compact: avoid pointless PThm rudiments; diff -r 706dac15554b -r 8088cf2576f3 src/Pure/Thy/export_theory.ML --- 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 diff -r 706dac15554b -r 8088cf2576f3 src/Pure/proofterm.ML --- 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 ();