diff --git a/src/Init/Lean/Elab/Tactic.lean b/src/Init/Lean/Elab/Tactic.lean
index 6616b75604..c08cf2b4c4 100644
--- a/src/Init/Lean/Elab/Tactic.lean
+++ b/src/Init/Lean/Elab/Tactic.lean
@@ -33,7 +33,7 @@ withMVarContext mvarId $ fun ctx s =>
   | EStateM.Result.ok a newS     => EStateM.Result.ok a newS.toTermState
 
 def reportUnsolvedGoals (ref : Syntax) (goals : List MVarId) : TermElabM Unit :=
-throwError ref $ "unsolved goals" ++ Format.line ++ MessageData.joinSep (goals.map $ MessageData.ofGoal) Format.line
+throwError ref $ "unsolved goals" ++ Format.line ++ MessageData.joinSep (goals.map $ MessageData.ofGoal) (Format.line ++ Format.line)
 
 def ensureAssignmentHasNoMVars (ref : Syntax) (mvarId : MVarId) : TermElabM Unit := do
 val ← instantiateMVars ref (mkMVar mvarId);