diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean
index f7b97e13c9..70ddf2bc33 100644
--- a/src/Lean/Elab/Syntax.lean
+++ b/src/Lean/Elab/Syntax.lean
@@ -458,12 +458,9 @@ def expandNotationItemIntoPattern (stx : Syntax) : CommandElabM Syntax :=
 /-- Try to derive a `SimpleDelab` from a notation.
     The notation must be of the form `notation ... => c var_1 ... var_n`
     where `c` is a declaration in the current scope and the `var_i` are a permutation of the LHS vars. -/
-def mkSimpleDelab (vars : Array Syntax) (pat qrhs : Syntax) : OptionT CommandElabM Syntax :=
+def mkSimpleDelab (vars : Array Syntax) (pat qrhs : Syntax) : OptionT CommandElabM Syntax := do
   match qrhs with
-  | `($c:ident $args*) => go c args
-  | `($c:ident)        => go c #[]
-  | _                  => failure
-  where go c args := do
+  | `($c:ident $args*) =>
     let [(c, [])] ← resolveGlobalName c.getId | failure
     guard <| args.all (Syntax.isIdent ∘ getAntiquotTerm)
     guard <| args.allDiff
@@ -472,6 +469,10 @@ def mkSimpleDelab (vars : Array Syntax) (pat qrhs : Syntax) : OptionT CommandEla
     `(@[appUnexpander $(mkIdent c):ident] def unexpand : Lean.PrettyPrinter.Unexpander := fun
        | `($qrhs) => `($pat)
        | _        => throw ())
+  | `($c:ident)        =>
+    let [(c, [])] ← resolveGlobalName c.getId | failure
+    `(@[appUnexpander $(mkIdent c):ident] def unexpand : Lean.PrettyPrinter.Unexpander := fun _ => `($pat))
+  | _                  => failure
 
 private def expandNotationAux (ref : Syntax)
     (currNamespace : Name) (attrKind : AttributeKind) (prec? : Option Syntax) (name? : Option Syntax) (prio? : Option Syntax) (items : Array Syntax) (rhs : Syntax) : CommandElabM Syntax := do
diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index 07fe65c6ce..34001968c9 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -141,13 +141,16 @@ def delabAppWithUnexpander : Delab := whenPPOption getPPNotation do
   let Expr.const c _ _ ← pure (← getExpr).getAppFn | failure
   let stx ← delabAppImplicit
   match stx with
-  | `($cPP:ident $args*) => do
+  | `($cPP:ident $args*) => do go c stx
+  | `($cPP:ident) => do go c stx
+  | _ => pure stx
+where
+  go c stx := do
     let some (f::_) ← pure <| (appUnexpanderAttribute.ext.getState (← getEnv)).table.find? c
       | pure stx
     let EStateM.Result.ok stx _ ← f stx |>.run ()
       | pure stx
     pure stx
-  | _ => pure stx
 
 /-- State for `delabAppMatch` and helpers. -/
 structure AppMatchState where
diff --git a/tests/lean/constDelab.lean b/tests/lean/constDelab.lean
new file mode 100644
index 0000000000..c631a2178c
--- /dev/null
+++ b/tests/lean/constDelab.lean
@@ -0,0 +1,2 @@
+notation "ℕ" => Nat
+#check ℕ
diff --git a/tests/lean/constDelab.lean.expected.out b/tests/lean/constDelab.lean.expected.out
new file mode 100644
index 0000000000..9b9ddacb87
--- /dev/null
+++ b/tests/lean/constDelab.lean.expected.out
@@ -0,0 +1 @@
+ℕ : Type