diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean
index dfada60b7e..688bb7aff2 100644
--- a/src/Lean/Elab/Binders.lean
+++ b/src/Lean/Elab/Binders.lean
@@ -55,7 +55,7 @@ partial def quoteAutoTactic : Syntax → TermElabM Syntax
         else
           let quotedArg ← quoteAutoTactic arg
           quotedArgs ← `(Array.push $quotedArgs $quotedArg)
-      `(Syntax.node $(quote k) $quotedArgs)
+      `(Syntax.node SourceInfo.none $(quote k) $quotedArgs)
   | Syntax.atom info val => `(mkAtom $(quote val))
   | Syntax.missing       => throwError "invalid auto tactic, tactic is missing"
 
diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean
index 34716cc4dd..3728d34e95 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/src/Lean/Elab/Quotation.lean
@@ -145,7 +145,7 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax
         else do
           let arg ← quoteSyntax arg
           args := args.push arg
-      `(Syntax.node $(quote k) $(args.build))
+      `(Syntax.node SourceInfo.none $(quote k) $(args.build))
   | Syntax.atom _ val =>
     `(Syntax.atom info $(quote val))
   | Syntax.missing => throwUnsupportedSyntax