# 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