diff --git a/src/Init/Lean/Meta/Exception.lean b/src/Init/Lean/Meta/Exception.lean
index 6b8ae87653..715be79fb7 100644
--- a/src/Init/Lean/Meta/Exception.lean
+++ b/src/Init/Lean/Meta/Exception.lean
@@ -92,9 +92,7 @@ def toTraceMessageData : Exception → MessageData
 | notInstance i ctx               => mkCtx ctx $ `notInstance ++ " " ++ i
 | appBuilder op msg args ctx      => mkCtx ctx $ `appBuilder ++ " " ++ op ++ " " ++ args ++ " " ++ msg
 | synthInstance inst ctx          => mkCtx ctx $ `synthInstance ++ " " ++ inst
-| tactic tacName mvarId msg ctx   =>
-  mkCtx ctx $ `tacticFailure ++ " " ++ tacName ++ " " ++ msg ++ Format.line ++
-    ppGoal ctx.env ctx.mctx ctx.lctx ctx.opts mvarId
+| tactic tacName mvarId msg ctx   => mkCtx ctx $ `tacticFailure ++ " " ++ tacName ++ " " ++ msg
 | bug _ _                         => "internal bug" -- TODO improve
 | other s                         => s
 
diff --git a/src/Init/Lean/Meta/Message.lean b/src/Init/Lean/Meta/Message.lean
index c13fa2005f..bab1b7d986 100644
--- a/src/Init/Lean/Meta/Message.lean
+++ b/src/Init/Lean/Meta/Message.lean
@@ -78,7 +78,9 @@ def toMessageData : Exception → MessageData
 | notInstance i ctx               => mkCtx ctx $ "not a type class instance " ++ i
 | appBuilder op msg args ctx      => mkCtx ctx $ "application builder failure " ++ op ++ " " ++ args ++ " " ++ msg
 | synthInstance inst ctx          => mkCtx ctx $ "failed to synthesize" ++ indentExpr inst
-| tactic tacName mvarId msg ctx   => "tactic '" ++ tacName ++ "' failed " ++ msg
+| tactic tacName mvarId msg ctx   =>
+  "tactic '" ++ tacName ++ "' failed " ++ msg ++ Format.line ++
+    ppGoal ctx.env ctx.mctx ctx.lctx ctx.opts mvarId
 | bug _ _                         => "internal bug" -- TODO improve
 | other s                         => s