diff --git a/src/Lean/Elab/Tactic/Split.lean b/src/Lean/Elab/Tactic/Split.lean
index 0cdc4d656b..53dd0c97a8 100644
--- a/src/Lean/Elab/Tactic/Split.lean
+++ b/src/Lean/Elab/Tactic/Split.lean
@@ -20,12 +20,12 @@ open Meta
       throwErrorAt stx[2] "'split' tactic failed, select a single target to split"
     if simplifyTarget then
       liftMetaTactic fun mvarId => do
-        let some mvarIds ← splitTarget? mvarId | throwError "'split' tactic failed"
+       let some mvarIds ← splitTarget? mvarId | Meta.throwTacticEx `split mvarId ""
         return mvarIds
     else
       let fvarId ← getFVarId hyps[0]
       liftMetaTactic fun mvarId => do
-        let some mvarIds ← splitLocalDecl? mvarId fvarId | throwError "'split' tactic failed"
+        let some mvarIds ← splitLocalDecl? mvarId fvarId | Meta.throwTacticEx `split mvarId ""
         return mvarIds
   | Location.wildcard =>
     liftMetaTactic fun mvarId => do
@@ -33,7 +33,7 @@ open Meta
       for fvarId in fvarIds do
         if let some mvarIds ← splitLocalDecl? mvarId fvarId then
           return mvarIds
-      let some mvarIds ← splitTarget? mvarId | throwError "'split' tactic failed"
+      let some mvarIds ← splitTarget? mvarId | Meta.throwTacticEx `split mvarId ""
       return mvarIds
 
 end Lean.Elab.Tactic
diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean
index 4c174550d4..957a4f07c6 100644
--- a/src/Lean/Message.lean
+++ b/src/Lean/Message.lean
@@ -59,6 +59,17 @@ inductive MessageData where
 
 namespace MessageData
 
+partial def isEmpty : MessageData → Bool
+  | ofFormat f => f.isEmpty
+  | withContext _ m => m.isEmpty
+  | withNamingContext _ m => m.isEmpty
+  | nest _ m => m.isEmpty
+  | group m => m.isEmpty
+  | compose m₁ m₂ => m₁.isEmpty && m₂.isEmpty
+  | tagged _ m => m.isEmpty
+  | node ms => ms.all (·.isEmpty)
+  | _ => false
+
 /- Instantiate metavariables occurring in nexted `ofExpr` constructors.
    It uses the surrounding `MetavarContext` at `withContext` constructors.
 -/
diff --git a/src/Lean/Meta/Tactic/Util.lean b/src/Lean/Meta/Tactic/Util.lean
index 79023bb51b..ac75471c4a 100644
--- a/src/Lean/Meta/Tactic/Util.lean
+++ b/src/Lean/Meta/Tactic/Util.lean
@@ -28,7 +28,10 @@ def mkFreshExprSyntheticOpaqueMVar (type : Expr) (tag : Name := Name.anonymous)
   mkFreshExprMVar type MetavarKind.syntheticOpaque tag
 
 def throwTacticEx {α} (tacticName : Name) (mvarId : MVarId) (msg : MessageData) (ref := Syntax.missing) : MetaM α :=
-  throwError "tactic '{tacticName}' failed, {msg}\n{MessageData.ofGoal mvarId}"
+  if msg.isEmpty then
+    throwError "tactic '{tacticName}' failed\n{MessageData.ofGoal mvarId}"
+  else
+    throwError "tactic '{tacticName}' failed, {msg}\n{MessageData.ofGoal mvarId}"
 
 def throwNestedTacticEx {α} (tacticName : Name) (ex : Exception) : MetaM α := do
   throwError "tactic '{tacticName}' failed, nested error:\n{ex.toMessageData}"