diff --git a/src/ast/macros/macro_manager.cpp b/src/ast/macros/macro_manager.cpp
index 032c724e1..bbe7f245c 100644
--- a/src/ast/macros/macro_manager.cpp
+++ b/src/ast/macros/macro_manager.cpp
@@ -175,12 +175,6 @@ namespace macro_manager_ns {
 /**
    \brief Mark all func_decls used in exprs as forbidden.
 */
-void macro_manager::mark_forbidden(unsigned n, expr * const * exprs) {
-    expr_mark visited;
-    macro_manager_ns::proc p(m_forbidden_set, m_forbidden);
-    for (unsigned i = 0; i < n; i++)
-        for_each_expr(p, visited, exprs[i]);
-}
 
 void macro_manager::mark_forbidden(unsigned n, justified_expr const * exprs) {
     expr_mark visited;
diff --git a/src/ast/macros/macro_manager.h b/src/ast/macros/macro_manager.h
index 57583b67b..a3c1a8d97 100644
--- a/src/ast/macros/macro_manager.h
+++ b/src/ast/macros/macro_manager.h
@@ -73,9 +73,7 @@ public:
     void push_scope();
     void pop_scope(unsigned num_scopes);
     void reset();
-    void mark_forbidden(unsigned n, expr * const * exprs);
     void mark_forbidden(unsigned n, justified_expr const * exprs);
-    void mark_forbidden(expr * e) { mark_forbidden(1, &e); }
     bool is_forbidden(func_decl * d) const { return m_forbidden_set.contains(d); }
     obj_hashtable<func_decl> const & get_forbidden_set() const { return m_forbidden_set; }
     void display(std::ostream & out);