diff --git a/src/ast/datatype_decl_plugin2.cpp b/src/ast/datatype_decl_plugin2.cpp
index a7d41dcbd..74750d2ca 100644
--- a/src/ast/datatype_decl_plugin2.cpp
+++ b/src/ast/datatype_decl_plugin2.cpp
@@ -361,7 +361,7 @@ namespace datatype {
             return true;
         }
 
-        void plugin::del(symbol const& s) {
+        void plugin::remove(symbol const& s) {
             def* d = 0;
             if (m_defs.find(s, d)) dealloc(d);
             m_defs.remove(s);
diff --git a/src/ast/datatype_decl_plugin2.h b/src/ast/datatype_decl_plugin2.h
index a5db0dbc6..3ea2ad1da 100644
--- a/src/ast/datatype_decl_plugin2.h
+++ b/src/ast/datatype_decl_plugin2.h
@@ -267,7 +267,7 @@ namespace datatype {
 
             def* mk(symbol const& name, unsigned n, sort * const * params);
 
-            void del(symbol const& d);
+            void remove(symbol const& d);
 
             bool mk_datatypes(unsigned num_datatypes, def * const * datatypes, unsigned num_params, sort* const* sort_params, sort_ref_vector & new_sorts);