diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index b0fd848fc1..0dd1082c7d 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -79,9 +79,9 @@ def optIdent : Parser := optional (try (ident >> " : "))
 def fromTerm   := parser! " from " >> termParser
 def haveAssign := parser! " := " >> termParser
 def haveDecl   := optIdent >> termParser >> (haveAssign <|> fromTerm <|> byTactic)
-@[builtinTermParser] def «have» := parser!:leadPrec "have " >> haveDecl >> "; " >> termParser
+@[builtinTermParser] def «have» := parser!:leadPrec withPosition ("have " >> haveDecl) >> optional "; " >> termParser
 def sufficesDecl := optIdent >> termParser >> fromTerm
-@[builtinTermParser] def «suffices» := parser!:leadPrec "suffices " >> sufficesDecl >> "; " >> termParser
+@[builtinTermParser] def «suffices» := parser!:leadPrec withPosition ("suffices " >> sufficesDecl) >> optional "; " >> termParser
 @[builtinTermParser] def «show»     := parser!:leadPrec "show " >> termParser >> (fromTerm <|> byTactic)
 def structInstArrayRef := parser! "[" >> termParser >>"]"
 def structInstLVal   := (ident <|> fieldIdx <|> structInstArrayRef) >> many (group ("." >> (ident <|> fieldIdx)) <|> structInstArrayRef)
@@ -156,14 +156,15 @@ def letPatDecl  := node `Lean.Parser.Term.letPatDecl  $ try (termParser >> pushN
 def letEqnsDecl := node `Lean.Parser.Term.letEqnsDecl $ letIdLhs >> matchAlts false
 -- Remark: we use `nodeWithAntiquot` here to make sure anonymous antiquotations (e.g., `$x`) are not `letDecl`
 def letDecl     := nodeWithAntiquot "letDecl" `Lean.Parser.Term.letDecl (notFollowedBy (nonReservedSymbol "rec") >> (letIdDecl <|> letPatDecl <|> letEqnsDecl))
-@[builtinTermParser] def «let» := parser!:leadPrec "let " >> letDecl >> "; " >> termParser
-@[builtinTermParser] def «let!» := parser!:leadPrec "let! " >> letDecl >> "; " >> termParser
+@[builtinTermParser] def «let» := parser!:leadPrec  withPosition ("let " >> letDecl) >> optional "; " >> termParser
+@[builtinTermParser] def «let!» := parser!:leadPrec withPosition ("let! " >> letDecl) >> optional "; " >> termParser
 def attrArg : Parser := ident <|> strLit <|> numLit
 -- use `rawIdent` because of attribute names such as `instance`
 def attrInstance     := parser! rawIdent >> many attrArg
 def attributes       := parser! "@[" >> sepBy1 attrInstance ", " >> "]"
 @[builtinTermParser] def «letrec» :=
-    parser!:leadPrec group ("let " >> nonReservedSymbol "rec ") >> sepBy1 (group (optional «attributes» >> letDecl)) ", " >> "; " >> termParser
+    parser!:leadPrec withPosition (group ("let " >> nonReservedSymbol "rec ") >> sepBy1 (group (optional «attributes» >> letDecl)) ", ")
+                     >> optional "; " >> termParser
 
 @[builtinTermParser] def nativeRefl   := parser! "nativeRefl! " >> termParser maxPrec
 @[builtinTermParser] def nativeDecide := parser! "nativeDecide! " >> termParser maxPrec
@@ -197,6 +198,7 @@ stx.isAntiquot || stx.isIdent
 @[builtinTermParser] def dollar     := tparser!:0 try (dollarSymbol >> checkWsBefore "expected space") >> termParser 0
 @[builtinTermParser] def dollarProj := tparser!:0 " $. " >> (fieldIdx <|> ident)
 
+-- TODO: fix
 @[builtinTermParser] def «where»    := tparser!:0 " where " >> sepBy1 letDecl (group ("; " >> symbol " where "))
 
 @[builtinTermParser] def fcomp  := tparser! infixR " ∘ " 90
@@ -249,8 +251,8 @@ stx.isAntiquot || stx.isIdent
 
 @[builtinTermParser] def panic       := parser!:leadPrec "panic! " >> termParser
 @[builtinTermParser] def unreachable := parser!:leadPrec "unreachable!"
-@[builtinTermParser] def dbgTrace    := parser!:leadPrec "dbgTrace! " >> termParser >> "; " >> termParser
-@[builtinTermParser] def assert      := parser!:leadPrec "assert! " >> termParser >> "; " >> termParser
+@[builtinTermParser] def dbgTrace    := parser!:leadPrec withPosition ("dbgTrace! " >> termParser) >> optional "; " >> termParser
+@[builtinTermParser] def assert      := parser!:leadPrec withPosition ("assert! " >> termParser) >> optional "; " >> termParser
 @[builtinTermParser] def «return»    := parser!:leadPrec "return " >> termParser
 
 end Term
diff --git a/tests/lean/run/def7.lean b/tests/lean/run/def7.lean
index 856b1fcb3b..e460585a32 100644
--- a/tests/lean/run/def7.lean
+++ b/tests/lean/run/def7.lean
@@ -39,6 +39,8 @@ theorem L.appendNil {α} : (as : L α) → append as nil = as
 | nil       => rfl
 | cons a as =>
   show cons a (fun _ => append (as ()) nil) = cons a as from
-  have ih : append (as ()) nil = as () from appendNil $ as ();
-  have thunkAux : (fun _ => as ()) = as from funext fun x => by { cases x; exact rfl };
+  have ih : append (as ()) nil = as () from appendNil $ as ()
+  have thunkAux : (fun _ => as ()) = as from funext fun x => by
+    cases x
+    exact rfl
   by rw [ih, thunkAux]; exact rfl
diff --git a/tests/lean/run/newfrontend1.lean b/tests/lean/run/newfrontend1.lean
index 01f66d02c2..14c4b8bd85 100644
--- a/tests/lean/run/newfrontend1.lean
+++ b/tests/lean/run/newfrontend1.lean
@@ -95,7 +95,7 @@ by {
   intro h1; intro _; intro h3;
   refine! Eq.trans ?pre ?post;
   exact y;
-  { exact h3 };
+  { exact h3 }
   { exact h1 }
 }
 
@@ -355,17 +355,17 @@ fun h1 _ h3 =>
 
 theorem simple22 (x y z : Nat) : y = z → y = x → id (x = z + 0) :=
 fun h1 h2 => show x = z + 0 by
-  apply Eq.trans;
-  exact h2.symm;
-  assumption;
+  apply Eq.trans
+  exact h2.symm
+  assumption
   skip
 
 theorem simple23 (x y z : Nat) : y = z → x = x → y = x → x = z :=
 fun h1 _ h3 =>
-  have x = y by { apply Eq.symm; assumption };
+  have x = y by apply Eq.symm; assumption
   Eq.trans this (by assumption)
 
 theorem simple24 (x y z : Nat) : y = z → x = x → y = x → x = z :=
 fun h1 _ h3 =>
-  have h : x = y by { apply Eq.symm; assumption };
+  have h : x = y by apply Eq.symm; assumption
   Eq.trans h (by assumption)