diff --git a/src/Lean/Parser/Extra.lean b/src/Lean/Parser/Extra.lean
index 20464de76f..c18ab9565c 100644
--- a/src/Lean/Parser/Extra.lean
+++ b/src/Lean/Parser/Extra.lean
@@ -48,20 +48,18 @@ attribute [runBuiltinParserAttributeHooks]
 
 end Parser
 
-namespace PrettyPrinter
-namespace Formatter
+section
+open PrettyPrinter
 
-@[combinatorFormatter Lean.Parser.ppHardSpace] def ppHardSpace.formatter : Formatter := push " "
-@[combinatorFormatter Lean.Parser.ppSpace] def ppSpace.formatter : Formatter := pushLine
-@[combinatorFormatter Lean.Parser.ppLine] def ppLine.formatter : Formatter := push "\n"
-@[combinatorFormatter Lean.Parser.ppGroup] def ppGroup.formatter (p : Formatter) : Formatter := group $ indent p
-@[combinatorFormatter Lean.Parser.ppIndent] def ppIndent.formatter (p : Formatter) : Formatter := indent p
+@[combinatorFormatter Lean.Parser.ppHardSpace] def ppHardSpace.formatter : Formatter := Formatter.push " "
+@[combinatorFormatter Lean.Parser.ppSpace] def ppSpace.formatter : Formatter := Formatter.pushLine
+@[combinatorFormatter Lean.Parser.ppLine] def ppLine.formatter : Formatter := Formatter.push "\n"
+@[combinatorFormatter Lean.Parser.ppGroup] def ppGroup.formatter (p : Formatter) : Formatter := Formatter.group $ Formatter.indent p
+@[combinatorFormatter Lean.Parser.ppIndent] def ppIndent.formatter (p : Formatter) : Formatter := Formatter.indent p
 @[combinatorFormatter Lean.Parser.ppDedent] def ppDedent.formatter (p : Formatter) : Formatter := do
   let opts ← getOptions
-  indent p (some (0 - Format.getIndent opts))
-
-end Formatter
-end PrettyPrinter
+  Formatter.indent p (some (0 - Format.getIndent opts))
+end
 
 namespace Parser
 
@@ -74,5 +72,15 @@ macro "registerParserAlias!" aliasName:strLit declName:ident : term =>
        PrettyPrinter.Formatter.registerAlias $aliasName $(mkIdentFrom declName (declName.getId ++ `formatter))
        PrettyPrinter.Parenthesizer.registerAlias $aliasName $(mkIdentFrom declName (declName.getId ++ `parenthesizer)))
 
+open PrettyPrinter in
+builtin_initialize
+  registerParserAlias! "group" group
+  registerParserAlias! "ppHardSpace" ppHardSpace
+  registerParserAlias! "ppSpace" ppSpace
+  registerParserAlias! "ppLine" ppLine
+  registerParserAlias! "ppGroup" ppGroup
+  registerParserAlias! "ppIndent" ppIndent
+  registerParserAlias! "ppDedent" ppDedent
+
 end Parser
 end Lean
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 07a2497d25..5b0a7c2b07 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -211,5 +211,13 @@ end Term
 
 @[builtinTermParser] def Level.quot  : Parser := parser! "`(level|" >> toggleInsideQuot levelParser >> ")"
 
+builtin_initialize
+  registerParserAlias! "letDecl"       Term.letDecl
+  registerParserAlias! "haveDecl"      Term.haveDecl
+  registerParserAlias! "sufficesDecl"  Term.sufficesDecl
+  registerParserAlias! "letRecDecls"   Term.letRecDecls
+  registerParserAlias! "hole"          Term.hole
+  registerParserAlias! "syntheticHole" Term.syntheticHole
+
 end Parser
 end Lean