clarified order of operations: no_thm_names first;

--- 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);