| changeset 74281 | 7829d6435c60 |
| parent 70821 | 37062fe19175 |
| child 74509 | f24ade4ff3cc |
--- a/src/Pure/logic.ML Thu Sep 09 23:05:33 2021 +0200 +++ b/src/Pure/logic.ML Thu Sep 09 23:07:02 2021 +0200 @@ -425,7 +425,8 @@ fun occs (t, u) = exists_subterm (fn s => t aconv s) u; (*Close up a formula over all free variables by quantification*) -fun close_form A = fold (all o Free) (Term.add_frees A []) A; +fun close_form A = + fold_rev (all o Free) (Frees.build (Frees.add_frees A) |> Frees.list_set) A;