diff --git a/src/Init/Lean/Elab/Quotation.lean b/src/Init/Lean/Elab/Quotation.lean
index a897f07156..01e116d28b 100644
--- a/src/Init/Lean/Elab/Quotation.lean
+++ b/src/Init/Lean/Elab/Quotation.lean
@@ -106,7 +106,7 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax
   let preresolved := resolveGlobalName env currNamespace openDecls val ++ preresolved;
   let val := quote val;
   -- `scp` is bound in stxQuot.expand
-  `(_app_ Syntax.ident none $(quote rawVal) (addMacroScope $val scp) $(quote preresolved))
+  `(_app_ Syntax.ident none $(quote rawVal) (_app_ addMacroScope $val scp) $(quote preresolved))
 -- if antiquotation, insert contents as-is, else recurse
 | stx@(Syntax.node k args) =>
   if isAntiquot stx then
@@ -272,7 +272,7 @@ private partial def compileStxMatch (ref : Syntax) : List Syntax → List Alt 
   let noAlts  := (alts.filter $ fun (alt : HeadInfo × Alt) => !info.generalizes alt.1).map Prod.snd;
   no ← withFreshMacroScope $ compileStxMatch (discr::discrs) noAlts;
   cond ← match info.argPats with
-  | some pats => `(_app_ Syntax.isOfKind discr $(quote kind) && _app_ Array.size (Syntax.getArgs discr) == $(quote pats.size))
+  | some pats => `(_app_ Syntax.isOfKind discr $(quote kind) && _app_ Array.size (_app_ Syntax.getArgs discr) == $(quote pats.size))
   | none      => `(_app_ Syntax.isOfKind discr $(quote kind));
   `(let discr := $discr; if _app_ coe $cond then $yes else $no)
 | _, _ => unreachable!
@@ -391,8 +391,8 @@ private unsafe partial def toPreterm : Syntax → TermElabM Expr
       pure $ lctx.mkLambda #[mkFVar n] e
   | `Lean.Parser.Term.app => do
     fn ← toPreterm $ args.get! 0;
-    arg ← toPreterm $ args.get! 1;
-    pure $ mkApp fn arg
+    as ← (args.get! 1).getArgs.mapM toPreterm;
+    pure $ mkAppN fn as
   | `Lean.Parser.Term.appCore => do
     fn ← toPreterm $ args.get! 1;
     as ← (args.get! 2).getArgs.mapM toPreterm;
diff --git a/src/Init/Lean/Parser/Term.lean b/src/Init/Lean/Parser/Term.lean
index 9b878747d7..5763a9ba29 100644
--- a/src/Init/Lean/Parser/Term.lean
+++ b/src/Init/Lean/Parser/Term.lean
@@ -112,7 +112,7 @@ def bracketedDoSeq := parser! "{" >> doSeq >> "}"
 @[builtinTermParser] def uminus := parser! "-" >> termParser 100
 
 def namedArgument  := tparser! try ("(" >> ident >> " := ") >> termParser >> ")"
-@[builtinTermParser] def app      := tparser! pushLeading >> (namedArgument <|> termParser appPrec)
+@[builtinTermParser] def app      := tparser! pushLeading >> many1 (namedArgument <|> termParser appPrec)
 
 -- Auxiliary notation used for fixing bootstrapping issues
 @[builtinTermParser] def appCore   := parser! "_app_ " >> termParser appPrec >> many1 (termParser appPrec)
@@ -183,7 +183,8 @@ end Parser
 open Parser
 
 def mkAppStx (fn : Syntax) (args : Array Syntax) : Syntax :=
-args.foldl (fun fn arg => Syntax.node `Lean.Parser.Term.app #[fn, arg]) fn
+Syntax.node `Lean.Parser.Term.app #[fn, mkNullNode args]
+-- args.foldl (fun fn arg => Syntax.node `Lean.Parser.Term.app #[fn, arg]) fn
 
 def mkHole (ref : Syntax) := mkNode `Lean.Parser.Term.hole #[mkAtomFrom ref "_"]