src/Pure/logic.ML
changeset 81516 31b05aef022d
parent 81512 c1aa8a61ee65
child 81542 e2ab4147b244
--- a/src/Pure/logic.ML	Sat Nov 30 17:14:30 2024 +0100
+++ b/src/Pure/logic.ML	Sat Nov 30 19:21:38 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 (Term.rename_wrt_term gi (strip_params gi))
+      val rfrees = map Free (rev (Term.variant_frees gi (strip_params gi)))
   in (gi, rfrees) end;
 
 fun concl_of_goal st i =