# 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