diff -r 8534f949548e -r 0da9433f959e src/Pure/logic.ML
--- a/src/Pure/logic.ML	Sat Jan 14 16:58:29 2012 +0100
+++ b/src/Pure/logic.ML	Sat Jan 14 17:45:04 2012 +0100
@@ -337,8 +337,7 @@
 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 =
-  Term.list_all_free (rev (Term.add_frees A []), A);
+fun close_form A = fold (all o Free) (Term.add_frees A []) A;