Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/logic.ML
changeset 81542 e2ab4147b244
parent 81516 31b05aef022d
child 81952 4652c6b36ee8 
--- 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 =
isabelle