diff --git a/src/Lean/PrettyPrinter.lean b/src/Lean/PrettyPrinter.lean
index e31f729b8b..fa8a42e37b 100644
--- a/src/Lean/PrettyPrinter.lean
+++ b/src/Lean/PrettyPrinter.lean
@@ -50,6 +50,9 @@ def ppConst (e : Expr) : MetaM Format := do
 def ppExprLegacy (env : Environment) (mctx : MetavarContext) (lctx : LocalContext) (opts : Options) (e : Expr) : IO Format :=
   Prod.fst <$> ((ppExpr e).run' { lctx := lctx } { mctx := mctx }).toIO { options := opts, fileName := "<PrettyPrinter>", fileMap := default } { env := env }
 
+def ppTactic (stx : Syntax) : CoreM Format :=
+  parenthesizeTactic stx >>= formatTactic
+
 def ppCommand (stx : Syntax) : CoreM Format :=
   parenthesizeCommand stx >>= formatCommand