diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index 61dbb01f0b..d170e0c4c9 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -64,19 +64,17 @@ open Meta
 @[builtinMacro Lean.Parser.Term.have] def expandHave : Macro := fun stx =>
   let thisId := mkIdentFrom stx `this
   match stx with
-  | `(have $x $bs* $[: $type]? := $val $[;]? $body)           => `(let_fun $x $bs* $[: $type]? := $val; $body)
-  | `(have : $type := $val $[;]? $body)                       => `(have $thisId : $type := $val; $body)
-  | `(have $x $bs* $[: $type]? $alts:matchAlts $[;]? $body)   => `(let_fun $x $bs* $[: $type]? $alts:matchAlts; $body)
-  | `(have : $type $alts:matchAlts $[;]? $body)               => `(have $thisId : $type $alts:matchAlts; $body)
-  | `(have $pattern:term := $val:term $[;]? $body)            => `(let_fun $pattern:term := $val:term ; $body)
-  | _                                                         => Macro.throwUnsupported
+  | `(have $x $bs* $[: $type]? := $val $[;]? $body)         => `(let_fun $x $bs* $[: $type]? := $val; $body)
+  | `(have $[: $type]? := $val $[;]? $body)                 => `(have $thisId:ident $[: $type]? := $val; $body)
+  | `(have $x $bs* $[: $type]? $alts:matchAlts $[;]? $body) => `(let_fun $x $bs* $[: $type]? $alts:matchAlts; $body)
+  | `(have $[: $type]? $alts:matchAlts $[;]? $body)         => `(have $thisId:ident $[: $type]? $alts:matchAlts; $body)
+  | `(have $pattern:term := $val:term $[;]? $body)          => `(let_fun $pattern:term := $val:term ; $body)
+  | _                                                       => Macro.throwUnsupported
 
 @[builtinMacro Lean.Parser.Term.suffices] def expandSuffices : Macro
-  | `(suffices $x:ident : $type from $val $[;]? $body)            => `(have $x : $type := $body; $val)
-  | `(suffices $type:term from $val $[;]? $body)                  => `(have : $type := $body; $val)
-  | `(suffices $x:ident : $type by%$b $tac:tacticSeq $[;]? $body) => `(have $x : $type := $body; by%$b $tac:tacticSeq)
-  | `(suffices $type:term by%$b $tac:tacticSeq $[;]? $body)       => `(have : $type := $body; by%$b $tac:tacticSeq)
-  | _                                                             => Macro.throwUnsupported
+  | `(suffices $[$x :]? $type from $val $[;]? $body)            => `(have $[$x]? : $type := $body; $val)
+  | `(suffices $[$x :]? $type by%$b $tac:tacticSeq $[;]? $body) => `(have $[$x]? : $type := $body; by%$b $tac:tacticSeq)
+  | _                                                           => Macro.throwUnsupported
 
 open Lean.Parser in
 private def elabParserMacroAux (prec : Syntax) (e : Syntax) : TermElabM Syntax := do
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 631495b573..559e4aeb8e 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -168,11 +168,9 @@ def letDecl     := nodeWithAntiquot "letDecl" `Lean.Parser.Term.letDecl (notFoll
 @[builtinTermParser] def «let_delayed» := leading_parser:leadPrec withPosition ("let_delayed " >> letDecl) >> optSemicolon termParser
 
 -- like `let_fun` but with optional name
-def haveIdLhs    := nodeWithAntiquot "haveIdLhs" `Lean.Parser.Term.haveIdLhs      <| ident >> checkWsBefore "expected space before binders" >> many (ppSpace >> (simpleBinderWithoutType <|> bracketedBinder)) >> optType
-def haveNoIdLhs  := nodeWithAntiquot "haveNoIdLhs" `Lean.Parser.Term.haveNoIdLhs  <| typeSpec
-def haveLhs      := haveIdLhs <|> haveNoIdLhs
-def haveIdDecl   := nodeWithAntiquot "haveIdDecl"   `Lean.Parser.Term.haveIdDecl   $ atomic (haveLhs >> " := ") >> termParser
-def haveEqnsDecl := nodeWithAntiquot "haveEqnsDecl" `Lean.Parser.Term.haveEqnsDecl $ haveLhs >> matchAlts
+def haveIdLhs    := optional (ident >> many (ppSpace >> (simpleBinderWithoutType <|> bracketedBinder))) >> optType
+def haveIdDecl   := nodeWithAntiquot "haveIdDecl"   `Lean.Parser.Term.haveIdDecl   $ atomic (haveIdLhs >> " := ") >> termParser
+def haveEqnsDecl := nodeWithAntiquot "haveEqnsDecl" `Lean.Parser.Term.haveEqnsDecl $ haveIdLhs >> matchAlts
 def haveDecl     := nodeWithAntiquot "haveDecl" `Lean.Parser.Term.haveDecl (haveIdDecl <|> letPatDecl <|> haveEqnsDecl)
 @[builtinTermParser] def «have» := leading_parser:leadPrec withPosition ("have " >> haveDecl) >> optSemicolon termParser
 
diff --git a/tests/lean/have.lean b/tests/lean/have.lean
index 93a26e765e..e9d5c8fd52 100644
--- a/tests/lean/have.lean
+++ b/tests/lean/have.lean
@@ -5,3 +5,7 @@ example : 5 = 3 :=
   have t : True := _
   have f : 5 = 6 := _
   f
+
+example : True :=
+  have := True.intro
+  this