diff -r 44c0028486db -r 31b05aef022d src/Pure/consts.ML
--- a/src/Pure/consts.ML	Sat Nov 30 17:14:30 2024 +0100
+++ b/src/Pure/consts.ML	Sat Nov 30 19:21:38 2024 +0100
@@ -313,7 +313,7 @@
 fun rev_abbrev lhs rhs =
   let
     val (xs, body) = strip_abss (Envir.beta_eta_contract rhs);
-    val vars = fold (fn (x, T) => cons (Var ((x, 0), T))) (Term.rename_wrt_term body xs) [];
+    val vars = map (fn (x, T) => Var ((x, 0), T)) (Term.variant_frees body xs);
   in (Term.subst_bounds (rev vars, body), Term.list_comb (lhs, vars)) end;
 
 in