diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index 7da4074e12..34bbf19500 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -185,8 +185,11 @@ private def expandFields (structStx : Syntax) (structModifiers : Modifiers) (str
           | some type =>
             let tac := binderTactic[2]
             let name ← Term.declareTacticSyntax tac
+            -- The tactic should be for binders+type.
+            -- It is safe to reset the binders to a "null" node since there is no value to be elaborated
+            let type ← `(forall $(binders.getArgs):bracketedBinder*, $type)
             let type ← `(autoParam $type $(mkIdentFrom tac name))
-            pure (binders, some type)
+            pure (mkNullNode, some type)
       else
         let (binders, type) := expandDeclSig fieldBinder[4]
         pure (binders, some type)