diff --git a/src/math/grobner/grobner.cpp b/src/math/grobner/grobner.cpp
index 329c08f92..59060b624 100644
--- a/src/math/grobner/grobner.cpp
+++ b/src/math/grobner/grobner.cpp
@@ -90,22 +90,6 @@ void grobner::unfreeze_equations(unsigned old_size) {
     m_equations_to_unfreeze.shrink(old_size);
 }
 
-void grobner::push_scope() {
-    m_scopes.push_back(scope());
-    scope & s = m_scopes.back();
-    s.m_equations_to_unfreeze_lim = m_equations_to_unfreeze.size();
-    s.m_equations_to_delete_lim   = m_equations_to_delete.size();
-}
-
-void grobner::pop_scope(unsigned num_scopes) {
-    SASSERT(num_scopes >= get_scope_level());
-    unsigned new_lvl = get_scope_level() - num_scopes;
-    scope & s        = m_scopes[new_lvl];
-    unfreeze_equations(s.m_equations_to_unfreeze_lim);
-    del_equations(s.m_equations_to_delete_lim);
-    m_scopes.shrink(new_lvl);
-}
-
 void grobner::reset() {
     flush();
     m_processed.reset();
@@ -312,7 +296,6 @@ grobner::monomial * grobner::mk_monomial(rational const & coeff, expr * m) {
 }
 
 void grobner::init_equation(equation * eq, v_dependency * d) {
-    eq->m_scope_lvl = get_scope_level();
     unsigned bidx   = m_equations_to_delete.size();
     eq->m_bidx      = bidx;
     eq->m_dep       = d;
@@ -626,10 +609,6 @@ grobner::equation * grobner::simplify(equation const * source, equation * target
             if (is_subset(LT, curr, rest)) {
                 if (i == 0)
                     m_changed_leading_term = true;
-                if (source->m_scope_lvl > target->m_scope_lvl) {
-                    target = copy_equation(target);
-                    SASSERT(target->m_scope_lvl >= source->m_scope_lvl);
-                }
                 if (!result) {
                     // first time that source is being applied.
                     target->m_dep = m_dep_manager.mk_join(target->m_dep, source->m_dep);
diff --git a/src/math/grobner/grobner.h b/src/math/grobner/grobner.h
index 9233866d5..c8668cf20 100644
--- a/src/math/grobner/grobner.h
+++ b/src/math/grobner/grobner.h
@@ -58,7 +58,6 @@ public:
     };
 
     class equation {
-        unsigned             m_scope_lvl;     //!< scope level when this equation was created.
         unsigned             m_bidx:31;       //!< position at m_equations_to_delete
         unsigned             m_lc:1;          //!< true if equation if a linear combination of the input equations.
         ptr_vector<monomial> m_monomials;     //!< sorted monomials
@@ -108,7 +107,6 @@ protected:
         unsigned m_equations_to_unfreeze_lim;
         unsigned m_equations_to_delete_lim;
     };
-    svector<scope>          m_scopes;
     ptr_vector<monomial>    m_tmp_monomials;
     ptr_vector<monomial>    m_del_monomials;
     ptr_vector<expr>        m_tmp_vars1;
@@ -192,8 +190,6 @@ public:
 
     ~grobner();
 
-    unsigned get_scope_level() const { return m_scopes.size(); }
-
     /**
        \brief Set the weight of a term that is viewed as a variable by this module.
        The weight is used to order monomials. If the weight is not set for a term t, then the
@@ -278,10 +274,6 @@ public:
 
     void get_equations(ptr_vector<equation> & result) const;
     
-    void push_scope();
-
-    void pop_scope(unsigned num_scopes);
-
     void display_equation(std::ostream & out, equation const & eq) const;
 
     void display_monomial(std::ostream & out, monomial const & m) const;