diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 1345f273ce..e0427c4a36 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -1336,6 +1336,16 @@ static bool is_atomic_notation(notation_entry const & entry) {
     return head(ts).get_action().kind() == notation::action_kind::Skip;
 }
 
+static format mk_tk_fmt(name const & tkn) {
+    auto tk = tkn.to_string();
+    if (!tk.empty() && tk.back() == ' ') {
+        tk.pop_back();
+        return format(tk) + line();
+    } else {
+        return format(tk);
+    }
+}
+
 auto pretty_fn::pp_notation(notation_entry const & entry, buffer<optional<expr>> & args) -> optional<result> {
     if (entry.is_numeral()) {
         return some(result(format(entry.get_num().to_string())));
@@ -1357,7 +1367,7 @@ auto pretty_fn::pp_notation(notation_entry const & entry, buffer<optional<expr>>
             format curr;
             notation::action const & a = ts[i].get_action();
             name const & tk = ts[i].get_token();
-            format tk_fmt = format(ts[i].get_pp_token());
+            format tk_fmt = mk_tk_fmt(ts[i].get_pp_token());
             switch (a.kind()) {
             case notation::action_kind::Skip:
                 curr = tk_fmt;
@@ -1502,7 +1512,7 @@ auto pretty_fn::pp_notation(notation_entry const & entry, buffer<optional<expr>>
             format e_fmt = pp_notation_child(e, token_lbp, 0).fmt();
             fmt = e_fmt + fmt;
         }
-        return optional<result>(result(first_lbp, last_rbp, fmt));
+        return optional<result>(result(first_lbp, last_rbp, group(nest(m_indent, fmt))));
     }
 }
 
diff --git a/tests/lean/elab13.lean.expected.out b/tests/lean/elab13.lean.expected.out
index 8dd3b6579a..af9ce94831 100644
--- a/tests/lean/elab13.lean.expected.out
+++ b/tests/lean/elab13.lean.expected.out
@@ -1,6 +1,8 @@
 λ (c : name),
-  get_env >>= λ (env : environment),
-    returnex (environment.get env c) >>= λ (decl : declaration),
-      return (length (declaration.univ_params decl)) >>= λ (num : ℕ),
-        mk_num_meta_univs 2 >>= λ (ls : list level), return (expr.const c ls) :
+  get_env >>=
+    λ (env : environment),
+      returnex (environment.get env c) >>=
+        λ (decl : declaration),
+          return (length (declaration.univ_params decl)) >>=
+            λ (num : ℕ), mk_num_meta_univs 2 >>= λ (ls : list level), return (expr.const c ls) :
   name → tactic expr
diff --git a/tests/lean/long_term.lean b/tests/lean/long_term.lean
new file mode 100644
index 0000000000..ba8e2844de
--- /dev/null
+++ b/tests/lean/long_term.lean
@@ -0,0 +1,18 @@
+def long_term :=
+(1+1+1+1+1+1+1+1+1)+
+(1+1+1+1+1+1+1+1+1)+
+(1+1+1+1+1+1+1+1+1)+
+(1+1+1+1+1+1+1+1+1)+
+(1+1+1+1+1+1+1+1+1)+
+(1+1+1+1+1+1+1+1+1)+
+(1+1+1+1+1+1+1+1+1) =
+(1+1+1+1+1+1+1+1+1)+
+(1+1+1+1+1+1+1+1+1)+
+(1+1+1+1+1+1+1+1+1)+
+(1+1+1+1+1+1+1+1+1)+
+(1+1+1+1+1+1+1+1+1)+
+(1+1+1+1+1+1+1+1+1)+
+(1+1+1+1+1+1+1+1+1)+
+(1+1+1+1+1+1+1+1+1)
+
+#print long_term
diff --git a/tests/lean/long_term.lean.expected.out b/tests/lean/long_term.lean.expected.out
new file mode 100644
index 0000000000..b7dbb7b806
--- /dev/null
+++ b/tests/lean/long_term.lean.expected.out
@@ -0,0 +1,12 @@
+def long_term : Prop :=
+1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + (1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1) + (1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1) +
+          (1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1) +
+        (1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1) +
+      (1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1) +
+    (1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1) =
+  1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + (1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1) + (1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1) +
+            (1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1) +
+          (1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1) +
+        (1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1) +
+      (1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1) +
+    (1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1)
diff --git a/tests/lean/print_meta.lean.expected.out b/tests/lean/print_meta.lean.expected.out
index 83e68630ce..54e150f8d0 100644
--- a/tests/lean/print_meta.lean.expected.out
+++ b/tests/lean/print_meta.lean.expected.out
@@ -1,4 +1,5 @@
 meta def tactic.intro : name → tactic expr :=
 λ (n : name),
-  tactic.target >>= λ (t : expr),
-    ite (↑(expr.is_pi t) ∨ ↑(expr.is_let t)) (tactic.intro_core n) (tactic.whnf_target >> tactic.intro_core n)
+  tactic.target >>=
+    λ (t : expr),
+      ite (↑(expr.is_pi t) ∨ ↑(expr.is_let t)) (tactic.intro_core n) (tactic.whnf_target >> tactic.intro_core n)