# HG changeset patch
# User wenzelm
# Date 1721592063 -7200
# Node ID 8b477e3e15fabee5fa70e159e90aa0f3f06f5644
# Parent  c5c53d0b61551b032f73a49981786a548e3737cd
clarified order of operations: no_thm_names first;

diff -r c5c53d0b6155 -r 8b477e3e15fa src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sun Jul 21 20:00:13 2024 +0200
+++ b/src/Pure/proofterm.ML	Sun Jul 21 22:01:03 2024 +0200
@@ -2167,11 +2167,11 @@
 
 fun export_proof thy i prop prf =
   let
-    val (prop', SOME prf') = (prop, SOME prf) |> standard_vars Name.context;
+    val (prop', SOME prf') = standard_vars Name.context (prop, SOME (no_thm_names prf));
     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;
 
-    val xml = (typargs, (args, (prop', no_thm_names prf'))) |>
+    val xml = (typargs, (args, (prop', prf'))) |>
       let
         open XML.Encode Term_XML.Encode;
         val encode_vars = list (pair string typ);