diff --git a/src/Init/Lean/Elab/BuiltinNotation.lean b/src/Init/Lean/Elab/BuiltinNotation.lean
index 8fcede142c..3cd8325824 100644
--- a/src/Init/Lean/Elab/BuiltinNotation.lean
+++ b/src/Init/Lean/Elab/BuiltinNotation.lean
@@ -13,8 +13,9 @@ namespace Term
 
 @[builtinTermElab dollar] def elabDollar : TermElab :=
 adaptExpander $ fun stx => match_syntax stx with
-| `($f $ $a) => `($f $a)
-| _          => throwUnsupportedSyntax
+| `($f $args* $ $a) => let args := args.push a; `($f $args*)
+| `($f $ $a)        => `($f $a)
+| _                 => throwUnsupportedSyntax
 
 @[builtinTermElab dollarProj] def elabDollarProj : TermElab :=
 adaptExpander $ fun stx => match_syntax stx with
diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean
index 84ba1ad973..02a1e77f7f 100644
--- a/src/Init/Lean/Elab/Term.lean
+++ b/src/Init/Lean/Elab/Term.lean
@@ -355,17 +355,10 @@ let instIdx := s.instImplicitIdx;
 modify $ fun s => { instImplicitIdx := s.instImplicitIdx + 1, .. s};
 pure $ (`_inst).appendIndexAfter instIdx
 
-/--
-  Return true if the given syntax is a `Lean.Parser.Term.cdot` or
-  is a `Lean.Parser.Term.app` containing a `cdot`.
-  We use this function as a filter to skip `expandCDotAux` (the expensive part)
-  at `expandCDot?` -/
-private partial def hasCDot : Syntax → Bool
-| stx =>
-  match_syntax stx with
-  | `(·)     => true
-  | `($f $a) => hasCDot f || hasCDot a
-  | _        => false
+private partial def isCDot (stx : Syntax) : Bool :=
+match_syntax stx with
+| `(·) => true
+| _    => false
 
 /--
   Auxiliary function for expandind the `·` notation.
@@ -381,37 +374,29 @@ withFreshMacroScope $
      pure id
   | _ => pure stx
 
-/--
-  Auxiliary function for expanding `·`s occurring as arguments of
-  applications (i.e., `Lean.Parser.Term.app` nodes).
-  Example: `foo · s` should expand into `foo _a_<idx> s` where
-  `_a_<idx>` is a fresh identifier. -/
-private partial def expandCDotInApp : Syntax → StateT (Array Syntax) TermElabM Syntax
-| n =>
-  match_syntax n with
-  | `($f $a) => do f ← expandCDotInApp f; a ← expandCDot a; `($f $a)
-  | n        => pure n
-
 /--
   Return `some` if succeeded expanding `·` notation occurring in
   the given syntax. Otherwise, return `none`.
   Examples:
   - `· + 1` => `fun _a_1 => _a_1 + 1`
   - `f · · b` => `fun _a_1 _a_2 => f _a_1 _a_2 b` -/
-def expandCDot? : Syntax → TermElabM (Option Syntax)
-| n@(Syntax.node k args) =>
-  if args.any hasCDot then
-    if k == `Lean.Parser.Term.app then do
-      (newNode, binders) ← (expandCDotInApp n).run #[];
-      `(fun $binders* => $newNode)
-    else do {
+def expandCDot? (stx : Syntax) : TermElabM (Option Syntax) :=
+match_syntax stx with
+| `($f $args*) =>
+   if args.any isCDot then do
+     (args, binders) ← (args.mapM expandCDot).run #[];
+     `(fun $binders* => $f $args*)
+   else
+     pure none
+| _ => match stx with
+  | Syntax.node k args =>
+    if args.any isCDot then do
       (args, binders) ← (args.mapM expandCDot).run #[];
       let newNode := Syntax.node k args;
       `(fun $binders* => $newNode)
-    }
-  else
-    pure none
-| _ => pure none
+    else
+      pure none
+  | _ => pure none
 
 private def exceptionToSorry (ref : Syntax) (errMsg : Message) (expectedType? : Option Expr) : TermElabM Expr := do
 expectedType : Expr ← match expectedType? with
diff --git a/src/Init/Lean/Elab/TermApp.lean b/src/Init/Lean/Elab/TermApp.lean
index 4c55fc4853..28903ef5a2 100644
--- a/src/Init/Lean/Elab/TermApp.lean
+++ b/src/Init/Lean/Elab/TermApp.lean
@@ -381,17 +381,21 @@ else
   else
     mergeFailures candidates f
 
-private partial def expandApp : Syntax → TermElabM (Syntax × Array NamedArg × Array Arg)
-| stx => match_syntax stx with
-  | `($fn ($id := $arg)) => do
-    (stx, namedArgs, args) ← expandApp fn;
-    namedArgs ← addNamedArg id namedArgs { name := id.getId, val := Arg.stx arg };
-    pure (stx, namedArgs, args)
-  | `($fn $arg)       => do
-    (stx, namedArgs, args) ← expandApp fn;
-    let args := args.push $ Arg.stx arg;
-    pure (stx, namedArgs, args)
-  | _                 => pure (stx, #[], #[])
+private partial def expandApp (stx : Syntax) : TermElabM (Syntax × Array NamedArg × Array Arg) := do
+let f    := stx.getArg 0;
+(namedArgs, args) ← (stx.getArg 1).getArgs.foldlM
+  (fun (acc : Array NamedArg × Array Arg) (stx : Syntax) => do
+    let (namedArgs, args) := acc;
+    if stx.getKind == `Lean.Parser.Term.namedArgument then do
+      -- tparser! try ("(" >> ident >> " := ") >> termParser >> ")"
+      let name := (stx.getArg 1).getId;
+      let val  := stx.getArg 3;
+      namedArgs ← addNamedArg stx namedArgs { name := name, val := Arg.stx val };
+      pure (namedArgs, args)
+    else
+      pure (namedArgs, args.push $ Arg.stx stx))
+  (#[], #[]);
+pure (f, namedArgs, args)
 
 @[builtinTermElab app] def elabApp : TermElab :=
 fun stx expectedType? => do
@@ -405,11 +409,14 @@ fun stx expectedType? =>
   let args := args.map Arg.stx;
   elabAppAux stx f #[] args expectedType?
 
-@[builtinTermElab «id»] def elabId : TermElab := elabApp
-@[builtinTermElab explicit] def elabExplicit : TermElab := elabApp
-@[builtinTermElab choice] def elabChoice : TermElab := elabApp
-@[builtinTermElab proj] def elabProj : TermElab := elabApp
-@[builtinTermElab arrayRef] def elabArrayRef : TermElab := elabApp
+def elabAtom : TermElab :=
+fun stx expectedType? => elabAppAux stx stx #[] #[] expectedType?
+
+@[builtinTermElab «id»] def elabId : TermElab := elabAtom
+@[builtinTermElab explicit] def elabExplicit : TermElab := elabAtom
+@[builtinTermElab choice] def elabChoice : TermElab := elabAtom
+@[builtinTermElab proj] def elabProj : TermElab := elabAtom
+@[builtinTermElab arrayRef] def elabArrayRef : TermElab := elabAtom
 
 @[builtinTermElab sortApp] def elabSortApp : TermElab :=
 fun stx _ => do
diff --git a/tests/compiler/termparsertest1.lean.expected.out b/tests/compiler/termparsertest1.lean.expected.out
index a630cb6c54..e7cacfc768 100644
--- a/tests/compiler/termparsertest1.lean.expected.out
+++ b/tests/compiler/termparsertest1.lean.expected.out
@@ -19,94 +19,94 @@ x.{max u v, 0}
    (null (Level.max "max" (null (Level.ident `u) (Level.ident `v))) "," (Level.num (numLit "0")))
    "}")))
 f 0 1
-(Term.app (Term.app (Term.id `f (null)) (Term.num (numLit "0"))) (Term.num (numLit "1")))
+(Term.app (Term.id `f (null)) (null (Term.num (numLit "0")) (Term.num (numLit "1"))))
 f.{u+1} "foo" x
 (Term.app
- (Term.app
-  (Term.id `f (null (Term.explicitUniv ".{" (null (Level.addLit (Level.ident `u) "+" (numLit "1"))) "}")))
-  (Term.str (strLit "\"foo\"")))
- (Term.id `x (null)))
+ (Term.id `f (null (Term.explicitUniv ".{" (null (Level.addLit (Level.ident `u) "+" (numLit "1"))) "}")))
+ (null (Term.str (strLit "\"foo\"")) (Term.id `x (null))))
 (f x, 0, 1)
 (Term.paren
  "("
  (null
-  (Term.app (Term.id `f (null)) (Term.id `x (null)))
+  (Term.app (Term.id `f (null)) (null (Term.id `x (null))))
   (null (Term.tupleTail "," (null (Term.num (numLit "0")) "," (Term.num (numLit "1"))))))
  ")")
 ()
 (Term.paren "(" (null) ")")
 (f x)
-(Term.paren "(" (null (Term.app (Term.id `f (null)) (Term.id `x (null))) (null)) ")")
+(Term.paren "(" (null (Term.app (Term.id `f (null)) (null (Term.id `x (null)))) (null)) ")")
 (f x : Type)
 (Term.paren
  "("
- (null (Term.app (Term.id `f (null)) (Term.id `x (null))) (null (Term.typeAscription ":" (Term.type "Type"))))
+ (null (Term.app (Term.id `f (null)) (null (Term.id `x (null)))) (null (Term.typeAscription ":" (Term.type "Type"))))
  ")")
 h (f x) (g y)
 (Term.app
- (Term.app (Term.id `h (null)) (Term.paren "(" (null (Term.app (Term.id `f (null)) (Term.id `x (null))) (null)) ")"))
- (Term.paren "(" (null (Term.app (Term.id `g (null)) (Term.id `y (null))) (null)) ")"))
+ (Term.id `h (null))
+ (null
+  (Term.paren "(" (null (Term.app (Term.id `f (null)) (null (Term.id `x (null)))) (null)) ")")
+  (Term.paren "(" (null (Term.app (Term.id `g (null)) (null (Term.id `y (null)))) (null)) ")")))
 if x then f x else g x
 (Term.if
  "if"
  (null)
  (Term.id `x (null))
  "then"
- (Term.app (Term.id `f (null)) (Term.id `x (null)))
+ (Term.app (Term.id `f (null)) (null (Term.id `x (null))))
  "else"
- (Term.app (Term.id `g (null)) (Term.id `x (null))))
+ (Term.app (Term.id `g (null)) (null (Term.id `x (null)))))
 if h : x then f x h else g x h
 (Term.if
  "if"
  (null `h ":")
  (Term.id `x (null))
  "then"
- (Term.app (Term.app (Term.id `f (null)) (Term.id `x (null))) (Term.id `h (null)))
+ (Term.app (Term.id `f (null)) (null (Term.id `x (null)) (Term.id `h (null))))
  "else"
- (Term.app (Term.app (Term.id `g (null)) (Term.id `x (null))) (Term.id `h (null))))
+ (Term.app (Term.id `g (null)) (null (Term.id `x (null)) (Term.id `h (null)))))
 have p x y from f x; g this
 (Term.have
  "have"
  (null)
- (Term.app (Term.app (Term.id `p (null)) (Term.id `x (null))) (Term.id `y (null)))
- (Term.fromTerm "from" (Term.app (Term.id `f (null)) (Term.id `x (null))))
+ (Term.app (Term.id `p (null)) (null (Term.id `x (null)) (Term.id `y (null))))
+ (Term.fromTerm "from" (Term.app (Term.id `f (null)) (null (Term.id `x (null)))))
  ";"
- (Term.app (Term.id `g (null)) (Term.id `this (null))))
+ (Term.app (Term.id `g (null)) (null (Term.id `this (null)))))
 suffices h : p x y from f x; g this
 (Term.suffices
  "suffices"
  (null `h ":")
- (Term.app (Term.app (Term.id `p (null)) (Term.id `x (null))) (Term.id `y (null)))
- (Term.fromTerm "from" (Term.app (Term.id `f (null)) (Term.id `x (null))))
+ (Term.app (Term.id `p (null)) (null (Term.id `x (null)) (Term.id `y (null))))
+ (Term.fromTerm "from" (Term.app (Term.id `f (null)) (null (Term.id `x (null)))))
  ";"
- (Term.app (Term.id `g (null)) (Term.id `this (null))))
+ (Term.app (Term.id `g (null)) (null (Term.id `this (null)))))
 show p x y from f x
 (Term.show
  "show"
- (Term.app (Term.app (Term.id `p (null)) (Term.id `x (null))) (Term.id `y (null)))
- (Term.fromTerm "from" (Term.app (Term.id `f (null)) (Term.id `x (null)))))
+ (Term.app (Term.id `p (null)) (null (Term.id `x (null)) (Term.id `y (null))))
+ (Term.fromTerm "from" (Term.app (Term.id `f (null)) (null (Term.id `x (null))))))
 fun x y => f y x
 (Term.fun
  "fun"
  (null (Term.id `x (null)) (Term.id `y (null)))
  "=>"
- (Term.app (Term.app (Term.id `f (null)) (Term.id `y (null))) (Term.id `x (null))))
+ (Term.app (Term.id `f (null)) (null (Term.id `y (null)) (Term.id `x (null)))))
 fun (x y : Nat) => f y x
 (Term.fun
  "fun"
  (null
   (Term.paren
    "("
-   (null (Term.app (Term.id `x (null)) (Term.id `y (null))) (null (Term.typeAscription ":" (Term.id `Nat (null)))))
+   (null (Term.app (Term.id `x (null)) (null (Term.id `y (null)))) (null (Term.typeAscription ":" (Term.id `Nat (null)))))
    ")"))
  "=>"
- (Term.app (Term.app (Term.id `f (null)) (Term.id `y (null))) (Term.id `x (null))))
+ (Term.app (Term.id `f (null)) (null (Term.id `y (null)) (Term.id `x (null)))))
 fun (x, y) => f y x
 (Term.fun
  "fun"
  (null (Term.paren "(" (null (Term.id `x (null)) (null (Term.tupleTail "," (null (Term.id `y (null)))))) ")"))
  "=>"
- (Term.app (Term.app (Term.id `f (null)) (Term.id `y (null))) (Term.id `x (null))))
+ (Term.app (Term.id `f (null)) (null (Term.id `y (null)) (Term.id `x (null)))))
 fun z (x, y) => f y x
 (Term.fun
  "fun"
@@ -114,7 +114,7 @@ fun z (x, y) => f y x
   (Term.id `z (null))
   (Term.paren "(" (null (Term.id `x (null)) (null (Term.tupleTail "," (null (Term.id `y (null)))))) ")"))
  "=>"
- (Term.app (Term.app (Term.id `f (null)) (Term.id `y (null))) (Term.id `x (null))))
+ (Term.app (Term.id `f (null)) (null (Term.id `y (null)) (Term.id `x (null)))))
 fun ⟨x, y⟩ ⟨z, w⟩ => f y x w z
 (Term.fun
  "fun"
@@ -122,19 +122,14 @@ fun ⟨x, y⟩ ⟨z, w⟩ => f y x w z
   (Term.anonymousCtor "⟨" (null (Term.id `x (null)) "," (Term.id `y (null))) "⟩")
   (Term.anonymousCtor "⟨" (null (Term.id `z (null)) "," (Term.id `w (null))) "⟩"))
  "=>"
- (Term.app
-  (Term.app (Term.app (Term.app (Term.id `f (null)) (Term.id `y (null))) (Term.id `x (null))) (Term.id `w (null)))
-  (Term.id `z (null))))
+ (Term.app (Term.id `f (null)) (null (Term.id `y (null)) (Term.id `x (null)) (Term.id `w (null)) (Term.id `z (null)))))
 fun (Prod.mk x y) => f y x
 (Term.fun
  "fun"
  (null
-  (Term.paren
-   "("
-   (null (Term.app (Term.app (Term.id `Prod.mk (null)) (Term.id `x (null))) (Term.id `y (null))) (null))
-   ")"))
+  (Term.paren "(" (null (Term.app (Term.id `Prod.mk (null)) (null (Term.id `x (null)) (Term.id `y (null)))) (null)) ")"))
  "=>"
- (Term.app (Term.app (Term.id `f (null)) (Term.id `y (null))) (Term.id `x (null))))
+ (Term.app (Term.id `f (null)) (null (Term.id `y (null)) (Term.id `x (null)))))
 { x := 10, y := 20 }
 (Term.structInst
  "{"
@@ -155,20 +150,14 @@ fun (Prod.mk x y) => f y x
   ",")
  "}")
 { x // p x 10 }
-(Term.subtype
- "{"
- `x
- (null)
- "//"
- (Term.app (Term.app (Term.id `p (null)) (Term.id `x (null))) (Term.num (numLit "10")))
- "}")
+(Term.subtype "{" `x (null) "//" (Term.app (Term.id `p (null)) (null (Term.id `x (null)) (Term.num (numLit "10")))) "}")
 { x : Nat // p x 10 }
 (Term.subtype
  "{"
  `x
  (null (Term.typeSpec ":" (Term.id `Nat (null))))
  "//"
- (Term.app (Term.app (Term.id `p (null)) (Term.id `x (null))) (Term.num (numLit "10")))
+ (Term.app (Term.id `p (null)) (null (Term.id `x (null)) (Term.num (numLit "10"))))
  "}")
 { .. }
 (Term.structInst "{" (null) (null (Term.structInstSource ".." (null))) "}")
@@ -181,17 +170,19 @@ fun (Prod.mk x y) => f y x
 a[i]
 (Term.arrayRef (Term.id `a (null)) "[" (Term.id `i (null)) "]")
 f [10, 20]
-(Term.app (Term.id `f (null)) (Term.listLit "[" (null (Term.num (numLit "10")) "," (Term.num (numLit "20"))) "]"))
+(Term.app
+ (Term.id `f (null))
+ (null (Term.listLit "[" (null (Term.num (numLit "10")) "," (Term.num (numLit "20"))) "]")))
 g a[x+2]
 (Term.app
  (Term.id `g (null))
- (Term.arrayRef (Term.id `a (null)) "[" (Term.add (Term.id `x (null)) "+" (Term.num (numLit "2"))) "]"))
+ (null (Term.arrayRef (Term.id `a (null)) "[" (Term.add (Term.id `x (null)) "+" (Term.num (numLit "2"))) "]")))
 g f.a.1.2.bla x.1.a
 (Term.app
- (Term.app
-  (Term.id `g (null))
-  (Term.proj (Term.proj (Term.proj (Term.id `f.a (null)) "." (fieldIdx "1")) "." (fieldIdx "2")) "." `bla))
- (Term.proj (Term.proj (Term.id `x (null)) "." (fieldIdx "1")) "." `a))
+ (Term.id `g (null))
+ (null
+  (Term.proj (Term.proj (Term.proj (Term.id `f.a (null)) "." (fieldIdx "1")) "." (fieldIdx "2")) "." `bla)
+  (Term.proj (Term.proj (Term.id `x (null)) "." (fieldIdx "1")) "." `a)))
 x+y*z < 10/3
 (Term.lt
  (Term.add (Term.id `x (null)) "+" (Term.mul (Term.id `y (null)) "*" (Term.id `z (null))))
@@ -199,8 +190,8 @@ x+y*z < 10/3
  (Term.div (Term.num (numLit "10")) "/" (Term.num (numLit "3"))))
 id (α := Nat) 10
 (Term.app
- (Term.app (Term.id `id (null)) (Term.namedArgument "(" `α ":=" (Term.id `Nat (null)) ")"))
- (Term.num (numLit "10")))
+ (Term.id `id (null))
+ (null (Term.namedArgument "(" `α ":=" (Term.id `Nat (null)) ")") (Term.num (numLit "10"))))
 (x : a)
 (Term.paren "(" (null (Term.id `x (null)) (null (Term.typeAscription ":" (Term.id `a (null))))) ")")
 a -> b
@@ -212,34 +203,36 @@ a -> b
  (Term.implicitBinder "{" (null `a) (null ":" (Term.type "Type")) "}")
  "->"
  (Term.depArrow
-  (Term.instBinder "[" (null) (Term.app (Term.id `HasToString (null)) (Term.id `a (null))) "]")
+  (Term.instBinder "[" (null) (Term.app (Term.id `HasToString (null)) (null (Term.id `a (null)))) "]")
   "->"
   (Term.depArrow (Term.explicitBinder "(" (null `x) (null ":" (Term.id `a (null))) (null) ")") "->" (Term.id `b (null)))))
 f ({x : a} -> b)
 (Term.app
  (Term.id `f (null))
- (Term.paren
-  "("
-  (null
-   (Term.depArrow (Term.implicitBinder "{" (null `x) (null ":" (Term.id `a (null))) "}") "->" (Term.id `b (null)))
-   (null))
-  ")"))
+ (null
+  (Term.paren
+   "("
+   (null
+    (Term.depArrow (Term.implicitBinder "{" (null `x) (null ":" (Term.id `a (null))) "}") "->" (Term.id `b (null)))
+    (null))
+   ")")))
 f (x : a) -> b
 (Term.arrow
  (Term.app
   (Term.id `f (null))
-  (Term.paren "(" (null (Term.id `x (null)) (null (Term.typeAscription ":" (Term.id `a (null))))) ")"))
+  (null (Term.paren "(" (null (Term.id `x (null)) (null (Term.typeAscription ":" (Term.id `a (null))))) ")")))
  "->"
  (Term.id `b (null)))
 f ((x : a) -> b)
 (Term.app
  (Term.id `f (null))
- (Term.paren
-  "("
-  (null
-   (Term.depArrow (Term.explicitBinder "(" (null `x) (null ":" (Term.id `a (null))) (null) ")") "->" (Term.id `b (null)))
-   (null))
-  ")"))
+ (null
+  (Term.paren
+   "("
+   (null
+    (Term.depArrow (Term.explicitBinder "(" (null `x) (null ":" (Term.id `a (null))) (null) ")") "->" (Term.id `b (null)))
+    (null))
+   ")")))
 (f : (n : Nat) → Vector Nat n) -> Nat
 (Term.depArrow
  (Term.explicitBinder
@@ -250,7 +243,7 @@ f ((x : a) -> b)
    (Term.depArrow
     (Term.explicitBinder "(" (null `n) (null ":" (Term.id `Nat (null))) (null) ")")
     "→"
-    (Term.app (Term.app (Term.id `Vector (null)) (Term.id `Nat (null))) (Term.id `n (null)))))
+    (Term.app (Term.id `Vector (null)) (null (Term.id `Nat (null)) (Term.id `n (null))))))
   (null)
   ")")
  "->"
@@ -274,7 +267,7 @@ match x with
  (null)
  "with"
  (null
-  (Term.matchAlt "|" (null (Term.app (Term.id `some (null)) (Term.id `x (null)))) "=>" (Term.id `true (null)))
+  (Term.matchAlt "|" (null (Term.app (Term.id `some (null)) (null (Term.id `x (null))))) "=>" (Term.id `true (null)))
   (Term.matchAlt "|" (null (Term.id `none (null))) "=>" (Term.id `false (null)))))
 
 match x with
@@ -291,7 +284,7 @@ match x with
  (null
   (Term.matchAlt
    "|"
-   (null (Term.app (Term.id `some (null)) (Term.id `y (null))))
+   (null (Term.app (Term.id `some (null)) (null (Term.id `y (null)))))
    "=>"
    (Term.match
     "match"
@@ -304,7 +297,7 @@ match x with
       (null
        (Term.app
         (Term.id `some (null))
-        (Term.paren "(" (null (Term.id `a (null)) (null (Term.tupleTail "," (null (Term.id `b (null)))))) ")")))
+        (null (Term.paren "(" (null (Term.id `a (null)) (null (Term.tupleTail "," (null (Term.id `b (null)))))) ")"))))
       "=>"
       (Term.add (Term.id `a (null)) "+" (Term.id `b (null))))
      (Term.matchAlt "|" (null (Term.id `none (null))) "=>" (Term.num (numLit "1"))))))
@@ -316,7 +309,7 @@ Sort v
 Type 1
 (Term.sortApp (Term.type "Type") (Level.num (numLit "1")))
 f Type 1
-(Term.app (Term.app (Term.id `f (null)) (Term.type "Type")) (Term.num (numLit "1")))
+(Term.app (Term.id `f (null)) (null (Term.type "Type") (Term.num (numLit "1"))))
 let x := 0; x + 1
 (Term.let
  "let"
@@ -339,7 +332,7 @@ let f (x : Nat) := x + 1; f 0
   ":="
   (Term.add (Term.id `x (null)) "+" (Term.num (numLit "1"))))
  ";"
- (Term.app (Term.id `f (null)) (Term.num (numLit "0"))))
+ (Term.app (Term.id `f (null)) (null (Term.num (numLit "0")))))
 let f {α : Type} (a : α) : α := a; f 10
 (Term.let
  "let"
@@ -352,7 +345,7 @@ let f {α : Type} (a : α) : α := a; f 10
   ":="
   (Term.id `a (null)))
  ";"
- (Term.app (Term.id `f (null)) (Term.num (numLit "10"))))
+ (Term.app (Term.id `f (null)) (null (Term.num (numLit "10")))))
 let f (x) := x + 1; f 10 + f 20
 (Term.let
  "let"
@@ -364,9 +357,9 @@ let f (x) := x + 1; f 10 + f 20
   (Term.add (Term.id `x (null)) "+" (Term.num (numLit "1"))))
  ";"
  (Term.add
-  (Term.app (Term.id `f (null)) (Term.num (numLit "10")))
+  (Term.app (Term.id `f (null)) (null (Term.num (numLit "10"))))
   "+"
-  (Term.app (Term.id `f (null)) (Term.num (numLit "20")))))
+  (Term.app (Term.id `f (null)) (null (Term.num (numLit "20"))))))
 let (x, y) := f 10; x + y
 (Term.let
  "let"
@@ -374,7 +367,7 @@ let (x, y) := f 10; x + y
   (Term.paren "(" (null (Term.id `x (null)) (null (Term.tupleTail "," (null (Term.id `y (null)))))) ")")
   (null)
   ":="
-  (Term.app (Term.id `f (null)) (Term.num (numLit "10"))))
+  (Term.app (Term.id `f (null)) (null (Term.num (numLit "10")))))
  ";"
  (Term.add (Term.id `x (null)) "+" (Term.id `y (null))))
 let { fst := x, .. } := f 10; x + x
@@ -388,13 +381,13 @@ let { fst := x, .. } := f 10; x + x
    "}")
   (null)
   ":="
-  (Term.app (Term.id `f (null)) (Term.num (numLit "10"))))
+  (Term.app (Term.id `f (null)) (null (Term.num (numLit "10")))))
  ";"
  (Term.add (Term.id `x (null)) "+" (Term.id `x (null))))
 let x.y := f 10; x
 (Term.let
  "let"
- (Term.letIdDecl `x.y (null) (null) ":=" (Term.app (Term.id `f (null)) (Term.num (numLit "10"))))
+ (Term.letIdDecl `x.y (null) (null) ":=" (Term.app (Term.id `f (null)) (null (Term.num (numLit "10")))))
  ";"
  (Term.id `x (null)))
 let x.1 := f 10; x
@@ -404,7 +397,7 @@ let x.1 := f 10; x
   (Term.proj (Term.id `x (null)) "." (fieldIdx "1"))
   (null)
   ":="
-  (Term.app (Term.id `f (null)) (Term.num (numLit "10"))))
+  (Term.app (Term.id `f (null)) (null (Term.num (numLit "10")))))
  ";"
  (Term.id `x (null)))
 let x[i].y := f 10; x
@@ -414,7 +407,7 @@ let x[i].y := f 10; x
   (Term.proj (Term.arrayRef (Term.id `x (null)) "[" (Term.id `i (null)) "]") "." `y)
   (null)
   ":="
-  (Term.app (Term.id `f (null)) (Term.num (numLit "10"))))
+  (Term.app (Term.id `f (null)) (null (Term.num (numLit "10")))))
  ";"
  (Term.id `x (null)))
 let x[i] := f 20; x
@@ -424,7 +417,7 @@ let x[i] := f 20; x
   (Term.arrayRef (Term.id `x (null)) "[" (Term.id `i (null)) "]")
   (null)
   ":="
-  (Term.app (Term.id `f (null)) (Term.num (numLit "20"))))
+  (Term.app (Term.id `f (null)) (null (Term.num (numLit "20")))))
  ";"
  (Term.id `x (null)))
 -x + y
@@ -446,18 +439,22 @@ do
  "do"
  (Term.doSeq
   (null
-   (Term.doId `x (null) "←" (Term.app (Term.id `f (null)) (Term.id `a (null))))
+   (Term.doId `x (null) "←" (Term.app (Term.id `f (null)) (null (Term.id `a (null)))))
    ";"
-   (Term.doId `x (null (Term.typeSpec ":" (Term.id `Nat (null)))) "←" (Term.app (Term.id `f (null)) (Term.id `a (null))))
+   (Term.doId
+    `x
+    (null (Term.typeSpec ":" (Term.id `Nat (null))))
+    "←"
+    (Term.app (Term.id `f (null)) (null (Term.id `a (null)))))
    ";"
-   (Term.doExpr (Term.app (Term.id `g (null)) (Term.id `x (null))))
+   (Term.doExpr (Term.app (Term.id `g (null)) (null (Term.id `x (null)))))
    ";"
-   (Term.doLet "let" (Term.letIdDecl `y (null) (null) ":=" (Term.app (Term.id `g (null)) (Term.id `x (null)))))
+   (Term.doLet "let" (Term.letIdDecl `y (null) (null) ":=" (Term.app (Term.id `g (null)) (null (Term.id `x (null))))))
    ";"
    (Term.doPat
     (Term.paren "(" (null (Term.id `a (null)) (null (Term.tupleTail "," (null (Term.id `b (null)))))) ")")
     "<-"
-    (Term.app (Term.app (Term.id `h (null)) (Term.id `x (null))) (Term.id `y (null)))
+    (Term.app (Term.id `h (null)) (null (Term.id `x (null)) (Term.id `y (null))))
     (null))
    ";"
    (Term.doLet
@@ -471,7 +468,7 @@ do
    (Term.doExpr
     (Term.app
      (Term.id `pure (null))
-     (Term.paren "(" (null (Term.add (Term.id `a (null)) "+" (Term.id `b (null))) (null)) ")"))))))
+     (null (Term.paren "(" (null (Term.add (Term.id `a (null)) "+" (Term.id `b (null))) (null)) ")")))))))
 do { x ← f a; pure $ a + a }
 (Term.do
  "do"
@@ -479,7 +476,7 @@ do { x ← f a; pure $ a + a }
   "{"
   (Term.doSeq
    (null
-    (Term.doId `x (null) "←" (Term.app (Term.id `f (null)) (Term.id `a (null))))
+    (Term.doId `x (null) "←" (Term.app (Term.id `f (null)) (null (Term.id `a (null)))))
     ";"
     (Term.doExpr (Term.dollar (Term.id `pure (null)) "$" (Term.add (Term.id `a (null)) "+" (Term.id `a (null)))))))
   "}"))
@@ -506,9 +503,9 @@ f 20
     "=>"
     (Term.mul (Term.id `n (null)) "*" (Term.id `b (null))))))
  ";"
- (Term.app (Term.id `f (null)) (Term.num (numLit "20"))))
+ (Term.app (Term.id `f (null)) (null (Term.num (numLit "20")))))
 max a b
-(Term.app (Term.app (Term.id `max (null)) (Term.id `a (null))) (Term.id `b (null)))
+(Term.app (Term.id `max (null)) (null (Term.id `a (null)) (Term.id `b (null))))
 f {x : a} -> b
 failed as expected, error: <input>:1:10 found '→' as expected, but brackets are needed
 (x := 20)
diff --git a/tests/lean/StxQuot.lean.expected.out b/tests/lean/StxQuot.lean.expected.out
index fb74b1e726..2e4a2a071e 100644
--- a/tests/lean/StxQuot.lean.expected.out
+++ b/tests/lean/StxQuot.lean.expected.out
@@ -9,9 +9,9 @@
 "(Command.declaration\n (Command.declModifiers (null) (null) (null) (null) (null) (null))\n (Command.def\n  \"def\"\n  (Command.declId `foo.0 (null))\n  (Command.optDeclSig (null) (null))\n  (Command.declValSimple \":=\" (Term.num (numLit \"1\")))))"
 "(null\n (Command.declaration\n  (Command.declModifiers (null) (null) (null) (null) (null) (null))\n  (Command.def\n   \"def\"\n   (Command.declId `foo.0 (null))\n   (Command.optDeclSig (null) (null))\n   (Command.declValSimple \":=\" (Term.num (numLit \"1\")))))\n (Command.declaration\n  (Command.declModifiers (null) (null) (null) (null) (null) (null))\n  (Command.def\n   \"def\"\n   (Command.declId `bar.0 (null))\n   (Command.optDeclSig (null) (null))\n   (Command.declValSimple \":=\" (Term.num (numLit \"2\"))))))"
 "(Term.id `Nat.one.0 (null))"
-"(Term.app (Term.app (Term.id `f.0 (null)) (Term.id `Nat.one.0 (null))) (Term.id `Nat.one.0 (null)))"
-"(Term.dollar\n (Term.id `f.0 (null))\n \"$\"\n (Term.app (Term.app (Term.id `f.0 (null)) (Term.id `Nat.one.0 (null))) (Term.num (numLit \"1\"))))"
-"(Term.app (Term.id `f.0 (null)) (Term.id `Nat.one.0 (null)))"
+"(Term.app (Term.id `f.0 (null)) (null (Term.id `Nat.one.0 (null)) (Term.id `Nat.one.0 (null))))"
+"(Term.dollar\n (Term.id `f.0 (null))\n \"$\"\n (Term.app (Term.id `f.0 (null)) (null (Term.id `Nat.one.0 (null)) (Term.num (numLit \"1\")))))"
+"(Term.app (Term.id `f.0 (null)) (null (Term.id `Nat.one.0 (null))))"
 "(Term.proj (Term.id `Nat.one.0 (null)) \".\" `b.0)"
 "(Term.add (Term.num (numLit \"2\")) \"+\" (Term.num (numLit \"1\")))"
 "(Command.declaration\n (Command.declModifiers (null) (null) (null) (null) (null) (null))\n (Command.def\n  \"def\"\n  (Command.declId `foo.0 (null))\n  (Command.optDeclSig (null) (null))\n  (Command.declValSimple \":=\" (Term.num (numLit \"1\")))))"