From fd85d4702e2763a6a4acc17f11b7db49217765c5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 9 Sep 2014 08:42:27 -0700
Subject: [PATCH] refactor(library/unifier): move all_local outside of the
 class

---
 src/library/unifier.cpp | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp
index 77d1abd76..7256e9a3d 100644
--- a/src/library/unifier.cpp
+++ b/src/library/unifier.cpp
@@ -264,6 +264,13 @@ static cnstr_group to_cnstr_group(unsigned d) {
     return static_cast<cnstr_group>(d);
 }
 
+/** \brief Return true if all arguments of lhs are local constants */
+static bool all_local(expr const & lhs) {
+    buffer<expr> margs;
+    get_app_args(lhs, margs);
+    return std::all_of(margs.begin(), margs.end(), [&](expr const & e) { return is_local(e); });
+}
+
 /** \brief Convert choice constraint delay factor to cnstr_group */
 cnstr_group get_choice_cnstr_group(constraint const & c) {
     lean_assert(is_choice_cnstr(c));
@@ -1652,13 +1659,6 @@ struct unifier_fn {
         return modified ? mk_app(m, margs) : lhs;
     }
 
-    /** \brief Return true if all arguments of lhs are local constants */
-    bool all_local(expr const & lhs) {
-        buffer<expr> margs;
-        get_app_args(lhs, margs);
-        return std::all_of(margs.begin(), margs.end(), [&](expr const & e) { return is_local(e); });
-    }
-
     optional<expr> expand_rhs(expr const & rhs, bool relax) {
         buffer<expr> args;
         expr const & f = get_app_rev_args(rhs, args);