# HG changeset patch
# User wenzelm
# Date 1721471743 -7200
# Node ID 166c61e21bfc4dedb7d3639d42ba2573279f1794
# Parent  ffef122946a301cd28f3d933cd891d09e9ebd98d
tuned: more direct Name.context for bounds;

diff -r ffef122946a3 -r 166c61e21bfc src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Fri Jul 19 22:29:32 2024 +0100
+++ b/src/Pure/proofterm.ML	Sat Jul 20 12:35:43 2024 +0200
@@ -2042,27 +2042,24 @@
 val declare_names_term' = fn SOME t => declare_names_term t | NONE => I;
 val declare_names_proof = fold_proof_terms declare_names_term;
 
-fun variant names bs x =
-  #1 (Name.variant x (fold Name.declare bs names));
-
 fun variant_term bs (Abs (x, T, t)) =
       let
-        val x' = variant (declare_names_term t Name.context) bs x;
-        val t' = variant_term (x' :: bs) t;
+        val x' = #1 (Name.variant x (declare_names_term t bs));
+        val t' = variant_term (Name.declare x' bs) t;
       in Abs (x', T, t') end
   | variant_term bs (t $ u) = variant_term bs t $ variant_term bs u
   | variant_term _ t = t;
 
 fun variant_proof bs (Abst (x, T, prf)) =
       let
-        val x' = variant (declare_names_proof prf Name.context) bs x;
-        val prf' = variant_proof (x' :: bs) prf;
+        val x' = #1 (Name.variant x (declare_names_proof prf bs));
+        val prf' = variant_proof (Name.declare x' bs) prf;
       in Abst (x', T, prf') end
   | variant_proof bs (AbsP (x, t, prf)) =
       let
-        val x' = variant (declare_names_term' t (declare_names_proof prf Name.context)) bs x;
+        val x' = #1 (Name.variant x (declare_names_term' t (declare_names_proof prf bs)));
         val t' = Option.map (variant_term bs) t;
-        val prf' = variant_proof (x' :: bs) prf;
+        val prf' = variant_proof (Name.declare x' bs) prf;
       in AbsP (x', t', prf') end
   | variant_proof bs (prf % t) = variant_proof bs prf % Option.map (variant_term bs) t
   | variant_proof bs (prf1 %% prf2) = variant_proof bs prf1 %% variant_proof bs prf2
@@ -2117,8 +2114,8 @@
       |> used_frees_term term
       |> fold used_frees_proof proofs;
     val inst = Term_Subst.zero_var_indexes_inst used_frees (term :: proof_terms);
-    val term' = term |> Term_Subst.instantiate inst |> unvarify |> variant_term [];
-    val proofs' = proofs |> map (instantiate inst #> unvarify_proof #> variant_proof []);
+    val term' = term |> Term_Subst.instantiate inst |> unvarify |> variant_term Name.context;
+    val proofs' = proofs |> map (instantiate inst #> unvarify_proof #> variant_proof Name.context);
   in (term', try hd proofs') end;
 
 fun standard_vars_term used t = #1 (standard_vars used (t, NONE));