diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index e7ea51981..d64cb92de 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -174,14 +174,6 @@ decl_info::decl_info(family_id family_id, decl_kind k, unsigned num_parameters,
     m_private_parameters(private_params) {
 }
 
-decl_info::decl_info(decl_info const& other) :
-    m_family_id(other.m_family_id),
-    m_kind(other.m_kind),
-    m_parameters(other.m_parameters.size(), other.m_parameters.data()),
-    m_private_parameters(other.m_private_parameters) {
-}
-
-
 void decl_info::init_eh(ast_manager & m) {
     for (parameter & p : m_parameters) {
         p.init_eh(m);
diff --git a/src/ast/ast.h b/src/ast/ast.h
index fb5072bc8..0fafc2a76 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -267,8 +267,6 @@ public:
     decl_info(family_id family_id = null_family_id, decl_kind k = null_decl_kind,
               unsigned num_parameters = 0, parameter const * parameters = nullptr, bool private_params = false);
 
-    decl_info(decl_info const& other);
-
     void init_eh(ast_manager & m);
     void del_eh(ast_manager & m);
 
@@ -368,8 +366,7 @@ public:
               unsigned num_parameters = 0, parameter const * parameters = nullptr, bool private_parameters = false):
         decl_info(family_id, k, num_parameters, parameters, private_parameters), m_num_elements(num_elements) {
     }
-    sort_info(sort_info const& other) : decl_info(other), m_num_elements(other.m_num_elements) {            
-    }
+
     sort_info(decl_info const& di, sort_size const& num_elements) : 
         decl_info(di), m_num_elements(num_elements) {}