# HG changeset patch
# User wenzelm
# Date 1717756754 -7200
# Node ID bc48bc7d0801260138eaf6d21f07daf04f118c33
# Parent  a3a1ec0c47ab35e68ff5a01d39074ea21d32e535
clarified signature: more explicit preprocessing;

diff -r a3a1ec0c47ab -r bc48bc7d0801 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Fri Jun 07 11:44:15 2024 +0200
+++ b/src/Pure/proofterm.ML	Fri Jun 07 12:39:14 2024 +0200
@@ -2146,11 +2146,8 @@
 
 local
 
-fun export_proof thy i prop prf0 =
+fun export_proof thy i prop prf =
   let
-    val prf = prf0
-      |> reconstruct_proof thy prop
-      |> apply_preproc thy;
     val (prop', SOME prf') = (prop, SOME prf) |> standard_vars Name.context;
     val args = [] |> add_standard_vars_term prop' |> add_standard_vars prf' |> rev;
     val typargs = [] |> Term.add_tfrees prop' |> fold_proof_terms Term.add_tfrees prf' |> rev;
@@ -2217,7 +2214,12 @@
 
     val exp_proof = Future.map proof_of body';
     val open_proof = not named ? rew_proof thy;
-    fun export_body () = Future.join exp_proof |> open_proof |> export_proof thy i prop1;
+    fun export_body () =
+      Future.join exp_proof
+      |> open_proof
+      |> reconstruct_proof thy prop1
+      |> apply_preproc thy
+      |> export_proof thy i prop1;
 
     val export =
       if export_enabled () then