src/Pure/Proof/proof_rewrite_rules.ML

--- a/src/Pure/Proof/proof_rewrite_rules.ML	Fri Nov 29 00:25:03 2024 +0100
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Fri Nov 29 11:26:17 2024 +0100
@@ -212,7 +212,8 @@
     fun rew_term Ts t =
       let
         val frees =
-          map Free (Name.invent (Term.declare_free_names t Name.context) "xa" (length Ts) ~~ Ts);
+          map Free
+            (Name.invent (Name.build_context (Term.declare_free_names t)) "xa" (length Ts) ~~ Ts);
         val t' = r (subst_bounds (frees, t));
         fun strip [] t = t
           | strip (_ :: xs) (Abs (_, _, t)) = strip xs t;