diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index 14a0a9d93c..2f9d74fb0b 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -162,8 +162,10 @@ private def declValToTerm (declVal : Syntax) : MacroM Syntax := withRef declVal
     expandMatchAltsWhereDecls declVal[0]
   else if declVal.isOfKind `Lean.Parser.Term.whereDecls then
     expandWhereDeclsAsStructInst declVal
+  else if declVal.isMissing then
+    Macro.throwErrorAt declVal "declaration body is missing"
   else
-    Macro.throwErrorAt declVal "unexpected definition value"
+    Macro.throwErrorAt declVal "unexpected declaration body"
 
 private def elabFunValues (headers : Array DefViewElabHeader) : TermElabM (Array Expr) :=
   headers.mapM fun header => withDeclName header.declName $ withLevelNames header.levelNames do
diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index aafba4f661..5aeb1a0612 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -34,7 +34,7 @@ def declSig          := leading_parser many (ppSpace >> (Term.simpleBinderWithou
 def optDeclSig       := leading_parser many (ppSpace >> (Term.simpleBinderWithoutType <|> Term.bracketedBinder)) >> Term.optType
 def declValSimple    := leading_parser " :=\n" >> termParser >> optional Term.whereDecls
 def declValEqns      := leading_parser Term.matchAltsWhereDecls
-def declVal          := declValSimple <|> declValEqns <|> Term.whereDecls
+def declVal          := declValSimple <|> declValEqns <|> Term.whereDecls <|> error "unexpected declaration body"
 def «abbrev»         := leading_parser "abbrev " >> declId >> optDeclSig >> declVal
 def «def»            := leading_parser "def " >> declId >> optDeclSig >> declVal
 def «theorem»        := leading_parser "theorem " >> declId >> declSig >> declVal