src/Pure/Syntax/syntax_trans.ML

 
 fun mark_bound_abs (x, T) = Const ("_bound", T --> T) $ Free (x, T);
 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;
 
 
 fun abs_tr' ctxt tm =
   uncurry (fold_rev (fn x => fn t => Syntax.const "_abs" $ x $ t))
     (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 =
   (case Ast.unfold_ast_p "_abs" (Ast.Appl (Ast.Constant "_abs" :: asts)) of
     ([], _) => raise Ast.AST ("abs_ast_tr'", asts)