--- a/src/HOL/Library/refute.ML Sat Nov 30 17:14:30 2024 +0100
+++ b/src/HOL/Library/refute.ML Sat Nov 30 19:21:38 2024 +0100
@@ -1186,8 +1186,8 @@
(a, T) :: strip_all_vars t
| strip_all_vars _ = [] : (string * typ) list
val strip_t = strip_all_body ex_closure
- val frees = Term.rename_wrt_term strip_t (strip_all_vars ex_closure)
- val subst_t = Term.subst_bounds (map Free frees, strip_t)
+ val frees = Term.variant_frees strip_t (strip_all_vars ex_closure)
+ val subst_t = Term.subst_bounds (map Free (rev frees), strip_t)
in
find_model ctxt (actual_params ctxt params) assm_ts subst_t true
end;