diff --git a/library/init/lean/syntax.lean b/library/init/lean/syntax.lean
index 98748489f2..ca093a51f5 100644
--- a/library/init/lean/syntax.lean
+++ b/library/init/lean/syntax.lean
@@ -34,7 +34,7 @@ inductive Syntax (α : Type := Unit)
 | missing {} : Syntax
 | node   (kind : SyntaxNodeKind) (args : Array Syntax) : Syntax
 | atom   {} (info : Option SourceInfo) (val : String) : Syntax
-| ident  {} (info : Option SourceInfo) (rawVal : Substring) (val : Name) (preresolved : List Name) : Syntax
+| ident  {} (info : Option SourceInfo) (rawVal : Substring) (val : Name) (preresolved : List (Nat × Name)) : Syntax
 | other  : α → Syntax
 
 instance stxInh {α} : Inhabited (Syntax α) :=