diff -r 8cbc8bc6f382 -r c1aa8a61ee65 src/Pure/Proof/proof_rewrite_rules.ML
--- a/src/Pure/Proof/proof_rewrite_rules.ML	Sat Nov 30 13:40:57 2024 +0100
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Sat Nov 30 13:41:38 2024 +0100
@@ -211,9 +211,8 @@
   let
     fun rew_term Ts t =
       let
-        val frees =
-          map Free
-            (Name.invent (Name.build_context (Term.declare_free_names t)) "xa" (length Ts) ~~ Ts);
+        val names = Name.build_context (Term.declare_free_names t);
+        val frees = map Free (Name.invent_names names "xa" Ts);
         val t' = r (subst_bounds (frees, t));
         fun strip [] t = t
           | strip (_ :: xs) (Abs (_, _, t)) = strip xs t;