diff --git a/lean4-mode/lean4-syntax.el b/lean4-mode/lean4-syntax.el
index fea289777a..249dcde17c 100644
--- a/lean4-mode/lean4-syntax.el
+++ b/lean4-mode/lean4-syntax.el
@@ -14,7 +14,7 @@
     "open" "export" "axiom" "inductive" "coinductive" "with" "without"
     "structure" "universe" "universes" "hide"
     "precedence" "reserve"
-    "match" "infix" "infixl" "infixr" "notation" "postfix" "prefix" "instance"
+    "match" "nomatch" "infix" "infixl" "infixr" "notation" "postfix" "prefix" "instance"
     "end" "this" "using" "using_well_founded" "namespace" "section"
     "attribute" "local" "set_option" "extends" "include" "omit" "classes" "class"
     "attributes" "raw" "replacing"
diff --git a/library/init/control/estate.lean b/library/init/control/estate.lean
index b26e42077f..ae85db241e 100644
--- a/library/init/control/estate.lean
+++ b/library/init/control/estate.lean
@@ -23,7 +23,7 @@ inductive Result.IsOk : Result ε σ α → Prop
 | mk (a : α) (s : σ) : Result.IsOk (Result.ok a s)
 
 theorem notIsOkError {e : ε} {s : σ} (h : @Result.IsOk _ _ α (Result.error e s)) : False :=
-match h with end
+nomatch h
 
 @[inline] def unreachableError {β : Type v} {e : ε} {s : σ} (h : @Result.IsOk _ _ α (Result.error e s)) : β :=
 False.elim (notIsOkError h)
diff --git a/library/init/data/int/basic.lean b/library/init/data/int/basic.lean
index f10bceaa98..3f1f585744 100644
--- a/library/init/data/int/basic.lean
+++ b/library/init/data/int/basic.lean
@@ -98,7 +98,7 @@ instance Int.DecidableEq : DecidableEq Int :=
 private def decNonneg (m : @& Int) : Decidable (NonNeg m) :=
 match m with
 | ofNat m   => isTrue $ NonNeg.mk m
-| negSucc m => isFalse $ fun h => match h with end
+| negSucc m => isFalse $ fun h => nomatch h
 
 @[extern cpp "lean::int_dec_le"]
 instance decLe (a b : @& Int) : Decidable (a ≤ b) :=
diff --git a/library/init/data/list/basic.lean b/library/init/data/list/basic.lean
index b2183993ec..78f98c66ae 100644
--- a/library/init/data/list/basic.lean
+++ b/library/init/data/list/basic.lean
@@ -301,9 +301,9 @@ instance [HasLess α] : HasLess (List α) :=
 ⟨List.Less⟩
 
 instance hasDecidableLt [HasLess α] [h : DecidableRel HasLess.Less] : ∀ (l₁ l₂ : List α), Decidable (l₁ < l₂)
-| []      []      := isFalse (fun h => match h with end)
+| []      []      := isFalse (fun h => nomatch h)
 | []      (b::bs) := isTrue (Less.nil _ _)
-| (a::as) []      := isFalse (fun h => match h with end)
+| (a::as) []      := isFalse (fun h => nomatch h)
 | (a::as) (b::bs) :=
   match h a b with
   | isTrue h₁  => isTrue (Less.head _ _ h₁)
diff --git a/library/init/lean/syntax.lean b/library/init/lean/syntax.lean
index 3a87a2ddb8..69dbbac778 100644
--- a/library/init/lean/syntax.lean
+++ b/library/init/lean/syntax.lean
@@ -47,14 +47,14 @@ inductive IsNode : Syntax → Prop
 
 def SyntaxNode : Type := {s : Syntax // IsNode s }
 
-def notIsNodeMissing (h : IsNode Syntax.missing) : False                   := match h with end
-def notIsNodeAtom   {info val} (h : IsNode (Syntax.atom info val)) : False := match h with end
-def notIsNodeIdent  {info rawVal val preresolved} (h : IsNode (Syntax.ident info rawVal val preresolved)) : False := match h with end
+def notIsNodeMissing (h : IsNode Syntax.missing) : False                   := nomatch h
+def notIsNodeAtom   {info val} (h : IsNode (Syntax.atom info val)) : False := nomatch h
+def notIsNodeIdent  {info rawVal val preresolved} (h : IsNode (Syntax.ident info rawVal val preresolved)) : False := nomatch h
 
 def unreachIsNodeMissing {α : Type} (h : IsNode Syntax.missing) : α := False.elim (notIsNodeMissing h)
 def unreachIsNodeAtom {α : Type} {info val} (h : IsNode (Syntax.atom info val)) : α := False.elim (notIsNodeAtom h)
 def unreachIsNodeIdent {α : Type} {info rawVal val preresolved} (h : IsNode (Syntax.ident info rawVal val preresolved)) : α :=
-False.elim (match h with end)
+False.elim (nomatch h)
 
 @[inline] def withArgs {α : Type} (n : SyntaxNode) (fn : Array Syntax → α) : α :=
 match n with
diff --git a/src/frontends/lean/match_expr.cpp b/src/frontends/lean/match_expr.cpp
index f4ed2e592f..fdf2eb5b40 100644
--- a/src/frontends/lean/match_expr.cpp
+++ b/src/frontends/lean/match_expr.cpp
@@ -40,13 +40,6 @@ expr parse_match(parser & p, unsigned, expr const *, pos_info const & pos) {
 
         p.check_token_next(get_with_tk(), "invalid 'match' expression, 'with' expected");
 
-        if (p.curr_is_token(get_end_tk())) {
-            /* Empty match */
-            p.next();
-            eqns.push_back(Fun(fn, mk_no_equation()));
-            expr f = p.save_pos(mk_equations(header, eqns.size(), eqns.data()), pos);
-            return p.mk_app(f, ts, pos);
-        }
         unsigned case_column = p.pos().second;
         if (is_eqn_prefix(p))
             p.next(); // optional '|' in the first case