From e83edefcc1664f2b9e5a2c6d20f1a72b3bf5605d Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 15 May 2020 14:39:40 +0200
Subject: [PATCH] fix: Syntax.setHeadInfo

---
 src/Init/Lean/Syntax.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Init/Lean/Syntax.lean b/src/Init/Lean/Syntax.lean
index e9e6b688e6..f60de6192a 100644
--- a/src/Init/Lean/Syntax.lean
+++ b/src/Init/Lean/Syntax.lean
@@ -233,9 +233,9 @@ partial def setHeadInfoAux (info : SourceInfo) : Syntax → Option Syntax
 | atom _ val             => some $ atom info val
 | ident _ rawVal val pre => some $ ident info rawVal val pre
 | node k args            =>
-  match updateFirst args setHeadInfoAux args.size with
+  match updateFirst args setHeadInfoAux 0 with
   | some args => some $ node k args
-  | noxne      => none
+  | noxne     => none
 | stx                    => none
 
 def setHeadInfo (stx : Syntax) (info : SourceInfo) : Syntax :=