diff -r 44c0028486db -r 31b05aef022d src/Pure/primitive_defs.ML
--- a/src/Pure/primitive_defs.ML	Sat Nov 30 17:14:30 2024 +0100
+++ b/src/Pure/primitive_defs.ML	Sat Nov 30 19:21:38 2024 +0100
@@ -77,8 +77,8 @@
 fun abs_def eq =
   let
     val body = Term.strip_all_body eq;
-    val vars = map Free (Term.rename_wrt_term body (Term.strip_all_vars eq));
-    val (lhs, rhs) = Logic.dest_equals (Term.subst_bounds (vars, body));
+    val vars = map Free (Term.variant_frees body (Term.strip_all_vars eq));
+    val (lhs, rhs) = Logic.dest_equals (Term.subst_bounds (rev vars, body));
     val (lhs', args) = Term.strip_comb lhs;
     val rhs' = fold_rev (absfree o dest_Free) args rhs;
   in (lhs', rhs') end;