diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index 905b7125dd..331bea1cbf 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -278,14 +278,15 @@ private partial def withFields {α}
       match type?, value? with
       | none,      none => throwError "invalid field, type expected"
       | some type, _    =>
-        withLocalDecl view.name view.binderInfo type $ fun fieldFVar =>
+        withLocalDecl view.name view.binderInfo type fun fieldFVar =>
           let infos := infos.push { name := view.name, declName := view.declName, fvar := fieldFVar, value? := value?,
                                     kind := StructFieldKind.newField, inferMod := view.inferMod }
           withFields views (i+1) infos k
       | none, some value =>
         let type ← inferType value
         withLocalDecl view.name view.binderInfo type fun fieldFVar =>
-          let infos := infos.push { name := view.name, declName := view.declName, fvar := fieldFVar, kind := StructFieldKind.newField, inferMod := view.inferMod }
+          let infos := infos.push { name := view.name, declName := view.declName, fvar := fieldFVar, value? := value,
+                                    kind := StructFieldKind.newField, inferMod := view.inferMod }
           withFields views (i+1) infos k
     | some info =>
       match info.kind with
diff --git a/tests/lean/run/fieldDefaultValueWithoutType.lean b/tests/lean/run/fieldDefaultValueWithoutType.lean
new file mode 100644
index 0000000000..238de1dde2
--- /dev/null
+++ b/tests/lean/run/fieldDefaultValueWithoutType.lean
@@ -0,0 +1,12 @@
+#lang lean4
+
+structure S :=
+(x := true)
+
+def f (s : S) : Bool :=
+s.x
+
+#eval f {}
+
+theorem ex : f {} = true :=
+rfl