diff -r 44c0028486db -r 31b05aef022d src/Pure/Syntax/syntax_trans.ML
--- a/src/Pure/Syntax/syntax_trans.ML	Sat Nov 30 17:14:30 2024 +0100
+++ b/src/Pure/Syntax/syntax_trans.ML	Sat Nov 30 19:21:38 2024 +0100
@@ -302,18 +302,18 @@
 fun mark_bound_body (x, T) = Const ("_bound", dummyT) $ Free (x, T);
 
 fun bound_vars vars body =
-  subst_bounds (map mark_bound_abs (Term.rename_wrt_term body vars), body);
+  subst_bounds (map mark_bound_abs (rev (Term.variant_frees body vars)), body);
 
 fun strip_abss vars_of body_of tm =
   let
     val vars = vars_of tm;
     val body = body_of tm;
-    val rev_new_vars = Term.rename_wrt_term body vars;
+    val new_vars = Term.variant_frees body vars;
     fun subst (x, T) b =
       if Name.is_internal x andalso not (Term.is_dependent b)
       then (Const ("_idtdummy", T), incr_boundvars ~1 b)
       else (mark_bound_abs (x, T), Term.subst_bound (mark_bound_body (x, T), b));
-    val (rev_vars', body') = fold_map subst rev_new_vars body;
+    val (rev_vars', body') = fold_map subst (rev new_vars) body;
   in (rev rev_vars', body') end;
 
 
@@ -322,7 +322,7 @@
     (strip_abss strip_abs_vars strip_abs_body (eta_contr ctxt tm));
 
 fun atomic_abs_tr' (x, T, t) =
-  let val [xT] = Term.rename_wrt_term t [(x, T)]
+  let val xT = singleton (Term.variant_frees t) (x, T)
   in (mark_bound_abs xT, subst_bound (mark_bound_body xT, t)) end;
 
 fun abs_ast_tr' asts =