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 =