diff --git a/src/kernel/expr_formatter.cpp b/src/kernel/expr_formatter.cpp
index cd5f05a9d..c257c22fc 100644
--- a/src/kernel/expr_formatter.cpp
+++ b/src/kernel/expr_formatter.cpp
@@ -8,6 +8,18 @@ Author: Leonardo de Moura
 #include "exception.h"
 
 namespace lean {
+
+format expr_formatter::operator()(char const * kwd, name const & n, expr const & t, expr const & v) {
+    format def = format{highlight_command(format(kwd)), space(), format(n), space(), colon(), space(),
+                        operator()(t), format(" :="), line(), operator()(v)};
+    return group(nest(def));
+}
+
+format expr_formatter::operator()(char const * kwd, name const & n, expr const & t) {
+    format def = format{highlight_command(format(kwd)), space(), format(n), space(), colon(), space(), operator()(t)};
+    return group(nest(def));
+}
+
 void expr_formatter::pp(std::ostream & out, expr const & e, context const & c) {
     out << mk_pair(operator()(e, c), get_options());
 }
diff --git a/src/kernel/expr_formatter.h b/src/kernel/expr_formatter.h
index c075cf602..51806ca74 100644
--- a/src/kernel/expr_formatter.h
+++ b/src/kernel/expr_formatter.h
@@ -16,6 +16,11 @@ public:
     virtual ~expr_formatter() {}
     /** \brief Convert expression in the given context into a format object. */
     virtual format operator()(expr const & e, context const & c = context()) = 0;
+    /** \brief format a definition. */
+    virtual format operator()(char const * kwd, name const & n, expr const & t, expr const & v);
+    /** \brief format a postulate. */
+    virtual format operator()(char const * kwd, name const & n, expr const & t);
+
     /** \brief Return options for pretty printing. */
     virtual options get_options() const = 0;
 
diff --git a/src/kernel/object.cpp b/src/kernel/object.cpp
index 18df9c48e..24049e681 100644
--- a/src/kernel/object.cpp
+++ b/src/kernel/object.cpp
@@ -36,9 +36,7 @@ bool         definition::is_opaque() const     { return m_opaque; }
 expr const & definition::get_value() const     { return m_value; }
 format       definition::pp(environment const & env) const {
     expr_formatter & fmt = env.get_formatter();
-    format def = format{highlight_command(format(keyword())), space(), format(get_name()), space(), colon(), space(),
-                        fmt(get_type()), format(" :="), line(), fmt(get_value())};
-    return group(fmt.nest(def));
+    return fmt(keyword(), get_name(), get_type(), get_value());
 }
 
 char const * theorem::g_keyword = "Theorem";
@@ -53,8 +51,7 @@ bool         fact::is_opaque() const     { lean_unreachable(); return false; }
 expr const & fact::get_value() const     { lean_unreachable(); return expr::null(); }
 format fact::pp(environment const & env) const {
     expr_formatter & fmt = env.get_formatter();
-    format def = format{highlight_command(format(keyword())), space(), format(get_name()), space(), colon(), space(), fmt(get_type())};
-    return group(fmt.nest(def));
+    return fmt(keyword(), get_name(), get_type());
 }
 
 char const * axiom::g_keyword = "Axiom";