diff --git a/src/Lean/Meta/PPGoal.lean b/src/Lean/Meta/PPGoal.lean
index 1ca8d65789..10cc6c2f7e 100644
--- a/src/Lean/Meta/PPGoal.lean
+++ b/src/Lean/Meta/PPGoal.lean
@@ -33,7 +33,7 @@ register_builtin_option pp.showLetValues : Bool := {
 }
 
 private def addLine (fmt : Format) : Format :=
-  if fmt.isNil then fmt else fmt ++ Format.line
+  if fmt.isNil then fmt else fmt ++ "\n"
 
 def getGoalPrefix (mvarDecl : MetavarDecl) : String :=
   if isLHSGoal? mvarDecl.type |>.isSome then
@@ -99,6 +99,6 @@ def ppGoal (mvarId : MVarId) : MetaM Format := do
       let fmt := fmt ++ getGoalPrefix mvarDecl ++ Format.nest indent typeFmt
       match mvarDecl.userName with
       | Name.anonymous => return fmt
-      | name           => return "case " ++ format name.eraseMacroScopes ++ Format.line ++ fmt
+      | name           => return "case " ++ format name.eraseMacroScopes ++ "\n" ++ fmt
 
 end Lean.Meta
diff --git a/tests/lean/issue2981.lean.expected.out b/tests/lean/issue2981.lean.expected.out
index 6551019d6c..284f10ec71 100644
--- a/tests/lean/issue2981.lean.expected.out
+++ b/tests/lean/issue2981.lean.expected.out
@@ -8,4 +8,5 @@ Tactic is run (ideally only twice, in most general context)
 Tactic is run (ideally only twice, in most general context)
 n : Nat
 ⊢ n < n.succ
-n m : Nat ⊢ n < n.succ
+n m : Nat
+⊢ n < n.succ
diff --git a/tests/lean/simpDisch.lean.expected.out b/tests/lean/simpDisch.lean.expected.out
index c6e58fe6a0..e7b4bfc6e4 100644
--- a/tests/lean/simpDisch.lean.expected.out
+++ b/tests/lean/simpDisch.lean.expected.out
@@ -8,7 +8,12 @@ h1 : x ≠ 0
 h2 : y ≠ 0
 h3 : x = y
 ⊢ x ≠ 0
-case simp.discharger x y : Nat h1 : x ≠ 0 h2 : y ≠ 0 h3 : x = y ⊢ y ≠ 0
+case simp.discharger
+x y : Nat
+h1 : x ≠ 0
+h2 : y ≠ 0
+h3 : x = y
+⊢ y ≠ 0
 x y : Nat
 h1 : x ≠ 0
 h2 : y ≠ 0