diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index 71318d583b..d860dd2368 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -324,7 +324,7 @@ syntax config := ("(" &"config" " := " term ")")
 syntax locationWildcard := "*"
 syntax locationHyp      := (colGt ident)+ ("⊢" <|> "|-")? -- TODO: delete
 syntax locationTargets  := (colGt ident)+ ("⊢" <|> "|-")?
-syntax location         := withPosition("at " locationWildcard <|> locationHyp)
+syntax location         := withPosition(" at " locationWildcard <|> locationHyp)
 
 syntax (name := change) "change " term (location)? : tactic
 syntax (name := changeWith) "change " term " with " term (location)? : tactic
diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index 2fa810a7f1..e67cc5a877 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -484,6 +484,7 @@ def format (formatter : Formatter) (stx : Syntax) : CoreM Format := do
     (fun _ => throwError "format: uncaught backtrack exception")
 
 def formatTerm := format $ categoryParser.formatter `term
+def formatTactic := format $ categoryParser.formatter `tactic
 def formatCommand := format $ categoryParser.formatter `command
 
 builtin_initialize registerTraceClass `PrettyPrinter.format;
diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean
index 8f500a3c65..77a89cb5cd 100644
--- a/src/Lean/PrettyPrinter/Parenthesizer.lean
+++ b/src/Lean/PrettyPrinter/Parenthesizer.lean
@@ -534,6 +534,7 @@ def parenthesize (parenthesizer : Parenthesizer) (stx : Syntax) : CoreM Syntax :
     (fun _ => throwError "parenthesize: uncaught backtrack exception")
 
 def parenthesizeTerm := parenthesize $ categoryParser.parenthesizer `term 0
+def parenthesizeTactic := parenthesize $ categoryParser.parenthesizer `tactic 0
 def parenthesizeCommand := parenthesize $ categoryParser.parenthesizer `command 0
 
 builtin_initialize registerTraceClass `PrettyPrinter.parenthesize