diff -r 5335b1ca6233 -r e2ab4147b244 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Mon Dec 02 22:16:29 2024 +0100
+++ b/src/Pure/logic.ML	Tue Dec 03 22:46:24 2024 +0100
@@ -667,7 +667,7 @@
 (*reverses parameters for substitution*)
 fun goal_params st i =
   let val gi = get_goal st i
-      val rfrees = map Free (rev (Term.variant_frees gi (strip_params gi)))
+      val rfrees = map Free (rev (Term.variant_bounds gi (strip_params gi)))
   in (gi, rfrees) end;
 
 fun concl_of_goal st i =