# HG changeset patch
# User wenzelm
# Date 1571132905 -7200
# Node ID f2ce687bfa0a7ab5c99261a824cbb4f9f2a4b536
# Parent  91b311e7d0405120ca62b7dc475fca36eac08594
apply_preproc for all proof boxes;

diff -r 91b311e7d040 -r f2ce687bfa0a src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Tue Oct 15 11:25:18 2019 +0200
+++ b/src/Pure/proofterm.ML	Tue Oct 15 11:48:25 2019 +0200
@@ -2135,10 +2135,12 @@
     val encode_proof = encode_standard_proof consts;
   in triple encode_vars encode_term encode_proof end;
 
-fun export_proof thy i prop prf =
+fun export_proof thy i prop prf0 =
   let
-    val (prop', SOME prf') =
-      standard_vars Name.context (prop, SOME (reconstruct_proof thy prop prf));
+    val prf = prf0
+      |> reconstruct_proof thy prop
+      |> apply_preproc thy;
+    val (prop', SOME prf') = (prop, SOME prf) |> standard_vars Name.context;
     val vars = [] |> add_standard_vars_term prop' |> add_standard_vars prf' |> rev;
     val xml = encode_export (Sign.consts_of thy) (vars, prop', prf');
     val chunks = Buffer.chunks (YXML.buffer_body xml Buffer.empty);
@@ -2169,10 +2171,9 @@
     val boxes = (proof, Inttab.empty) |-> export_boxes |> Inttab.dest;
   in List.app (Lazy.force o #2) boxes end;
 
-fun export thy i prop prf0 =
+fun export thy i prop prf =
   if export_enabled () then
     let
-      val prf = apply_preproc thy prf0;
       val _ = force_export_boxes prf;
       val _ = export_proof thy i prop prf;
     in () end