diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp
index 8b5f941c8..509e15ff7 100644
--- a/src/ast/ast_smt2_pp.cpp
+++ b/src/ast/ast_smt2_pp.cpp
@@ -431,6 +431,7 @@ format_ns::format * smt2_pp_environment::pp_sort(sort * s) {
         fs.push_back(pp_sort(to_sort(s->get_parameter(0).get_ast())));
         return mk_seq1(m, fs.begin(), fs.end(), f2f(), get_sutil().is_seq(s)?"Seq":"Re");
     }
+#if 0
     if (get_dtutil().is_datatype(s)) {
         ptr_buffer<format> fs;
         unsigned sz = get_dtutil().get_datatype_num_parameter_sorts(s);
@@ -439,6 +440,7 @@ format_ns::format * smt2_pp_environment::pp_sort(sort * s) {
         }
         return mk_seq1(m, fs.begin(), fs.end(), f2f(), s->get_name().str().c_str());        
     }
+#endif
     return format_ns::mk_string(get_manager(), s->get_name().str().c_str());
 }
 
diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp
index 8cf3965cf..fe02f24a0 100644
--- a/src/ast/ast_smt_pp.cpp
+++ b/src/ast/ast_smt_pp.cpp
@@ -366,13 +366,14 @@ class smt_printer {
             return;
         }
         else if (s->is_sort_of(m_dt_fid, DATATYPE_SORT)) {
+            m_out << m_renaming.get_symbol(s->get_name());            
+#if 0
             datatype_util util(m_manager);
             unsigned num_sorts = util.get_datatype_num_parameter_sorts(s);
             if (num_sorts > 0) {
                 m_out << "(";
             }
 
-            m_out << m_renaming.get_symbol(s->get_name());            
             if (num_sorts > 0) {
                 for (unsigned i = 0; i < num_sorts; ++i) {
                     m_out << " ";
@@ -380,6 +381,7 @@ class smt_printer {
                 }
                 m_out << ")";
             }
+#endif
             return;
         }
         else {
diff --git a/src/util/lp/lp_settings_instances.cpp b/src/util/lp/lp_settings_instances.cpp
index e9a3888ba..ac2ed4b51 100644
--- a/src/util/lp/lp_settings_instances.cpp
+++ b/src/util/lp/lp_settings_instances.cpp
@@ -2,8 +2,8 @@
   Copyright (c) 2017 Microsoft Corporation
   Author: Lev Nachmanson
 */
-#include "util/vector.h"
 #include <memory>
+#include "util/vector.h"
 #include "util/lp/lp_settings.hpp"
 template bool lean::vectors_are_equal<double>(vector<double> const&, vector<double> const&);
 template bool lean::vectors_are_equal<lean::mpq>(vector<lean::mpq > const&, vector<lean::mpq> const&);
diff --git a/src/util/lp/row_eta_matrix_instances.cpp b/src/util/lp/row_eta_matrix_instances.cpp
index c32023164..c172eda11 100644
--- a/src/util/lp/row_eta_matrix_instances.cpp
+++ b/src/util/lp/row_eta_matrix_instances.cpp
@@ -2,8 +2,8 @@
   Copyright (c) 2017 Microsoft Corporation
   Author: Lev Nachmanson
 */
-#include "util/vector.h"
 #include <memory>
+#include "util/vector.h"
 #include "util/lp/row_eta_matrix.hpp"
 #include "util/lp/lu.h"
 namespace lean {