--- 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;