# HG changeset patch # User wenzelm # Date 1572792346 -3600 # Node ID be689b7d81fdc45b49a42850a1cd52ca52aedb90 # Parent bb403cb94db25cc94a373c82ddd37584038313e0 clarified signature -- more options; diff -r bb403cb94db2 -r be689b7d81fd src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Sun Nov 03 10:29:01 2019 +0000 +++ b/src/Pure/Proof/proof_syntax.ML Sun Nov 03 15:45:46 2019 +0100 @@ -15,7 +15,8 @@ val proof_of: bool -> thm -> Proofterm.proof val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T val pretty_standard_proof_of: Proof.context -> bool -> thm -> Pretty.T - val pretty_proof_boxes_of: Proof.context -> bool -> thm -> Pretty.T + val pretty_proof_boxes_of: Proof.context -> + {full: bool, preproc: theory -> proof -> proof} -> thm -> Pretty.T end; structure Proof_Syntax : PROOF_SYNTAX = @@ -253,7 +254,7 @@ fun pretty_standard_proof_of ctxt full thm = pretty_proof ctxt (Thm.standard_proof_of {full = full, expand_name = Thm.expand_name thm} thm); -fun pretty_proof_boxes_of ctxt full thm = +fun pretty_proof_boxes_of ctxt {full, preproc} thm = let val thy = Proof_Context.theory_of ctxt; val selection = @@ -264,7 +265,9 @@ |> map (fn ({serial = i, pos, prop, ...}, proof) => let val proof' = proof - |> full ? Proofterm.reconstruct_proof thy prop + |> Proofterm.reconstruct_proof thy prop + |> preproc thy + |> not full ? Proofterm.shrink_proof |> Proofterm.forall_intr_variables prop; val prop' = prop |> Proofterm.forall_intr_variables_term; diff -r bb403cb94db2 -r be689b7d81fd src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Sun Nov 03 10:29:01 2019 +0000 +++ b/src/Pure/proofterm.ML Sun Nov 03 15:45:46 2019 +0100 @@ -151,6 +151,7 @@ val add_prf_rrule: proof * proof -> theory -> theory val add_prf_rproc: (typ list -> term option list -> proof -> (proof * proof) option) -> theory -> theory val set_preproc: (theory -> proof -> proof) -> theory -> theory + val apply_preproc: theory -> proof -> proof val forall_intr_variables_term: term -> term val forall_intr_variables: term -> proof -> proof val no_skel: proof