diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 500ee23e060..952f2ad43e0 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -2330,10 +2330,6 @@ namespace lp {
         return true;
     }
 
-    void lar_solver::pivot_column_tableau(unsigned j, unsigned row_index) {
-        m_mpq_lar_core_solver.m_r_solver.pivot_column_tableau(j, row_index);
-        m_mpq_lar_core_solver.m_r_solver.change_basis(j, r_basis()[row_index]);
-    }
 } // namespace lp
 
 
diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index 83d2a25fe29..a321632fb61 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -519,8 +519,6 @@ class lar_solver : public column_namer {
         return m_mpq_lar_core_solver.lower_bound(j);
     }
 
-    void pivot_column_tableau(unsigned j, unsigned row_index);
-    
     inline const impq & column_upper_bound(unsigned j) const {
         return m_mpq_lar_core_solver.upper_bound(j);
     }