diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index f2d024da42..49b63e1c60 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -959,7 +959,8 @@ fun stx expectedType? => do
 
 @[builtinTermElab «namedHole»] def elabNamedHole : TermElab :=
 fun stx expectedType? => do
-  let name := stx.getIdAt 1;
+  let arg  := stx.getArg 1;
+  let name := if arg.isIdent then arg.getId else Name.anonymous;
   mvar ← mkFreshExprMVar expectedType? MetavarKind.syntheticOpaque name;
   registerMVarErrorContext mvar.mvarId! stx;
   pure mvar
diff --git a/src/Lean/Parser/Tactic.lean b/src/Lean/Parser/Tactic.lean
index a5d191ad9b..ee5c8fd579 100644
--- a/src/Lean/Parser/Tactic.lean
+++ b/src/Lean/Parser/Tactic.lean
@@ -65,11 +65,11 @@ def matchAlts : Parser := withPosition $ fun pos => (optional "| ") >> sepBy1 ma
 @[builtinTacticParser] def orelse := tparser!:2 " <|> " >> tacticParser 1
 
 /- Term binders as tactics. They are all implemented as macros using the triad: named holes, hygiene, and `refine` tactic. -/
-@[builtinTacticParser] def «have»     := parser! "have " >> Term.optIdent >> termParser >> (Term.haveAssign <|> Term.fromTerm) >> "; " >> tacticParser
-@[builtinTacticParser] def «suffices» := parser! "suffices " >> Term.optIdent >> termParser >> Term.fromTerm >> "; " >> tacticParser
-@[builtinTacticParser] def «show»     := parser! "show " >> termParser >> " from " >> tacticParser
-@[builtinTacticParser] def «let»      := parser! "let "  >> Term.letDecl >> "; " >> tacticParser
-@[builtinTacticParser] def «let!»     := parser! "let! " >> Term.letDecl >> "; " >> tacticParser
+@[builtinTacticParser] def «have»     := parser! "have " >> Term.haveDecl
+@[builtinTacticParser] def «suffices» := parser! "suffices " >> Term.sufficesDecl
+@[builtinTacticParser] def «show»     := parser! "show " >> termParser
+@[builtinTacticParser] def «let»      := parser! "let "  >> Term.letDecl
+@[builtinTacticParser] def «let!»     := parser! "let! " >> Term.letDecl
 
 end Tactic
 end Parser
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index b3ee679ea3..ce2f9edfc3 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -53,7 +53,7 @@ def leadPrec := maxPrec - 1
 @[builtinTermParser] def sort := parser! "Sort" >> optional (checkWsBefore "" >> checkPrec (maxPrec-1) >> levelParser maxPrec)
 @[builtinTermParser] def prop := parser! "Prop"
 @[builtinTermParser] def hole := parser! "_"
-@[builtinTermParser] def namedHole := parser! "?" >> ident
+@[builtinTermParser] def namedHole := parser! "?" >> (ident <|> hole)
 @[builtinTermParser] def «sorry» := parser! "sorry"
 @[builtinTermParser] def cdot   := parser! "·"
 @[builtinTermParser] def emptyC := parser! "∅"
@@ -66,8 +66,10 @@ def optIdent : Parser := optional (try (ident >> " : "))
 @[builtinTermParser] def «if»  := parser!:leadPrec "if " >> optIdent >> termParser >> " then " >> termParser >> " else " >> termParser
 def fromTerm   := parser! " from " >> termParser
 def haveAssign := parser! " := " >> termParser
-@[builtinTermParser] def «have» := parser!:leadPrec "have " >> optIdent >> termParser >> (haveAssign <|> fromTerm) >> "; " >> termParser
-@[builtinTermParser] def «suffices» := parser!:leadPrec "suffices " >> optIdent >> termParser >> fromTerm >> "; " >> termParser
+def haveDecl   := optIdent >> termParser >> (haveAssign <|> fromTerm)
+@[builtinTermParser] def «have» := parser!:leadPrec "have " >> haveDecl >> "; " >> termParser
+def sufficesDecl := optIdent >> termParser >> fromTerm
+@[builtinTermParser] def «suffices» := parser!:leadPrec "suffices " >> sufficesDecl >> "; " >> termParser
 @[builtinTermParser] def «show»     := parser!:leadPrec "show " >> termParser >> fromTerm
 def structInstArrayRef := parser! "[" >> termParser >>"]"
 def structInstLVal   := (ident <|> fieldIdx <|> structInstArrayRef) >> many (group ("." >> (ident <|> fieldIdx)) <|> structInstArrayRef)