diff --git a/src/util/lp/nla_core.cpp b/src/util/lp/nla_core.cpp
index c9aea09ce..2718139f0 100644
--- a/src/util/lp/nla_core.cpp
+++ b/src/util/lp/nla_core.cpp
@@ -21,25 +21,6 @@ Revision History:
 #include "util/lp/factorization_factory_imp.h"
 namespace nla {
 
-
-point operator+(const point& a, const point& b) {
-    return point(a.x + b.x, a.y + b.y);
-} 
-
-point operator-(const point& a, const point& b) {
-    return point(a.x - b.x, a.y - b.y);
-} 
-unsigned core::find_monomial(const unsigned_vector& k) const {
-    TRACE("nla_solver_find", tout << "k = "; print_product_with_vars(k, tout););
-    auto it = m_mkeys.find(k);
-    if (it == m_mkeys.end()) {
-        TRACE("nla_solver", tout << "not found";);
-        return -1;
-    }
-    TRACE("nla_solver", tout << "found " << it->second << ", mon = "; print_monomial_with_vars(m_monomials[it->second], tout););
-    return it->second;
-}
-    
 core::core(lp::lar_solver& s) :
     m_evars(),
     m_lar_solver(s),
diff --git a/src/util/lp/nla_core.h b/src/util/lp/nla_core.h
index 7504bb4c7..5a06f16d7 100644
--- a/src/util/lp/nla_core.h
+++ b/src/util/lp/nla_core.h
@@ -104,9 +104,7 @@ struct core {
     std::unordered_map<unsigned_vector, unsigned, hash_svector>      m_mkeys; // the key is the sorted vars of a monomial 
     tangents                                                         m_tangents;
     basics                                                            m_basics;
-    // methods
-    unsigned find_monomial(const unsigned_vector& k) const;
-    core(lp::lar_solver& s, reslimit& lim, params_ref const& p);
+    core(lp::lar_solver& s);
     
     bool compare_holds(const rational& ls, llc cmp, const rational& rs) const;