diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean
index f1cf91a4fc..31d7d3d7db 100644
--- a/src/Lean/Elab/Declaration.lean
+++ b/src/Lean/Elab/Declaration.lean
@@ -348,7 +348,7 @@ def elabMutual : CommandElab := fun stx => do
         throwErrorAt bad "invalid 'decreasing_by' in 'mutual' block, it must be used after the 'end' keyword"
     elabMutualDef stx[1].getArgs hints
   else
-    throwError "invalid mutual block"
+    throwError "invalid mutual block: either all elements of the block must be inductive declarations, or they must all be definitions/theorems/abbrevs"
 
 /- leading_parser "attribute " >> "[" >> sepBy1 (eraseAttr <|> Term.attrInstance) ", " >> "]" >> many1 ident -/
 @[builtin_command_elab «attribute»] def elabAttr : CommandElab := fun stx => do
diff --git a/tests/lean/invalidMutualError.lean b/tests/lean/invalidMutualError.lean
new file mode 100644
index 0000000000..a338f9c3ef
--- /dev/null
+++ b/tests/lean/invalidMutualError.lean
@@ -0,0 +1,17 @@
+/-! Test invalid mutual block error message -/
+
+inductive Foo : Type where
+  | foo0 : Nat → Foo
+  | foo1 : Foo → Foo
+  | foo2 : Foo → Foo → Foo
+
+mutual
+
+  inductive Bar1 : Foo → Prop where
+    | mk {f : Foo} : Bar f → Bar1 (.foo1 f)
+
+  def Bar : Foo → Prop
+    | .foo1 f => Bar1 f
+    | _ => True
+
+end
\ No newline at end of file
diff --git a/tests/lean/invalidMutualError.lean.expected.out b/tests/lean/invalidMutualError.lean.expected.out
new file mode 100644
index 0000000000..9f47fc1e0c
--- /dev/null
+++ b/tests/lean/invalidMutualError.lean.expected.out
@@ -0,0 +1 @@
+invalidMutualError.lean:8:0-17:3: error: invalid mutual block: either all elements of the block must be inductive declarations, or they must all be definitions/theorems/abbrevs