diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h
index e2b1eb682..b74515566 100644
--- a/src/util/lp/lar_solver.h
+++ b/src/util/lp/lar_solver.h
@@ -34,25 +34,24 @@ namespace lean {
 
 class lar_solver : public column_namer {
     //////////////////// fields //////////////////////////
-    lp_settings m_settings;
-    stacked_value<lp_status> m_status;
-    stacked_value<simplex_strategy_enum> m_simplex_strategy;
+    lp_settings                             m_settings;
+    stacked_value<lp_status>                m_status;
+    stacked_value<simplex_strategy_enum>    m_simplex_strategy;
     std::unordered_map<unsigned, var_index> m_ext_vars_to_columns;
-    vector<unsigned> m_columns_to_ext_vars_or_term_indices;
-    stacked_vector<ul_pair> m_vars_to_ul_pairs;
-    vector<lar_base_constraint*> m_constraints;
-    stacked_value<unsigned> m_constraint_count;
+    vector<unsigned>                        m_columns_to_ext_vars_or_term_indices;
+    stacked_vector<ul_pair>                 m_vars_to_ul_pairs;
+    vector<lar_base_constraint*>            m_constraints;
+    stacked_value<unsigned>                 m_constraint_count;
     // the set of column indices j such that bounds have changed for j
-    int_set m_columns_with_changed_bound;
-    int_set m_rows_with_changed_bounds;
-    int_set m_basic_columns_with_changed_cost;
-    stacked_value<int> m_infeasible_column_index; // such can be found at the initialization step
-    stacked_value<unsigned> m_term_count;
-    vector<lar_term*> m_terms;
-    vector<lar_term*> m_orig_terms;
-    const var_index m_terms_start_index;
-    indexed_vector<mpq> m_column_buffer;    
-    std::function<column_type (unsigned)> m_column_type_function;    
+    int_set                                 m_columns_with_changed_bound;
+    int_set                                 m_rows_with_changed_bounds;
+    int_set                                 m_basic_columns_with_changed_cost;
+    stacked_value<int>                      m_infeasible_column_index; // such can be found at the initialization step
+    stacked_value<unsigned>                 m_term_count;
+    vector<lar_term*>                       m_terms;
+    vector<lar_term*>                       m_orig_terms;
+    const var_index                         m_terms_start_index;
+    indexed_vector<mpq>                     m_column_buffer;    
 public:
     lar_core_solver m_mpq_lar_core_solver;
     unsigned constraint_count() const {
@@ -83,7 +82,6 @@ public:
     lar_solver() : m_status(OPTIMAL),
                    m_infeasible_column_index(-1),
                    m_terms_start_index(1000000),
-                   m_column_type_function ([this] (unsigned j) {return m_mpq_lar_core_solver.m_column_types()[j];}),
                    m_mpq_lar_core_solver(m_settings, *this)
     {}