diff --git a/src/library/print.cpp b/src/library/print.cpp
index e7df3735ce..48282f6693 100644
--- a/src/library/print.cpp
+++ b/src/library/print.cpp
@@ -147,6 +147,10 @@ struct print_expr_fn {
         print_child(app_arg(e));
     }
 
+    static bool is_arrow(expr const & t) {
+        return lean::is_arrow(t) && binding_info(t) == binder_info::Default;
+    }
+
     void print_arrow_body(expr const & a) {
         if (is_atomic(a) || is_arrow(a))
             return print(a);