diff --git a/src/kernel/formatter.cpp b/src/kernel/formatter.cpp
index 594d61fbb..051c01cb1 100644
--- a/src/kernel/formatter.cpp
+++ b/src/kernel/formatter.cpp
@@ -30,12 +30,10 @@ struct print_expr_fn {
     }
 
     void print_macro(expr const & a, context const & c) {
-        if (macro_num_args(a) > 0) out() << "(";
         macro_def(a).display(out());
         for (unsigned i = 0; i < macro_num_args(a); i++) {
             out() << " "; print_child(macro_arg(a, i), c);
         }
-        if (macro_num_args(a) > 0) out() << ")";
     }
 
     void print_sort(expr const & a) {