diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index 9a1976b960..8496c9d5a3 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -500,7 +500,7 @@ private def elabFieldTypeValue (view : StructFieldView) : TermElabM (Option Expr
         Term.synthesizeSyntheticMVarsNoPostponing
         -- TODO: add forbidden predicate using `shortDeclName` from `view`
         let params ← Term.addAutoBoundImplicits params
-        let value ← Term.elabTerm valStx none
+        let value ← Term.withoutAutoBoundImplicit <| Term.elabTerm valStx none
         let value ← mkLambdaFVars params value
         return (none, value)
     | some typeStx =>
@@ -512,7 +512,7 @@ private def elabFieldTypeValue (view : StructFieldView) : TermElabM (Option Expr
         let type  ← mkForallFVars params type
         return (type, none)
       | some valStx =>
-        let value ← Term.elabTermEnsuringType valStx type
+        let value ← Term.withoutAutoBoundImplicit <| Term.elabTermEnsuringType valStx type
         Term.synthesizeSyntheticMVarsNoPostponing
         let type  ← mkForallFVars params type
         let value ← mkLambdaFVars params value
diff --git a/tests/lean/autoImplicitForbidden.lean b/tests/lean/autoImplicitForbidden.lean
index 54b54dca31..9cc11570ae 100644
--- a/tests/lean/autoImplicitForbidden.lean
+++ b/tests/lean/autoImplicitForbidden.lean
@@ -21,3 +21,10 @@ mutual
 
   inductive Ex2 : Type
 end
+
+
+structure Bar :=
+  (x : Na)
+  (y : Nat := foobar)  -- Error at `foobar`
+
+#print Bar.mk
diff --git a/tests/lean/autoImplicitForbidden.lean.expected.out b/tests/lean/autoImplicitForbidden.lean.expected.out
index 33c9afc685..dc28113019 100644
--- a/tests/lean/autoImplicitForbidden.lean.expected.out
+++ b/tests/lean/autoImplicitForbidden.lean.expected.out
@@ -3,3 +3,5 @@ autoImplicitForbidden.lean:6:10-6:11: error: unknown identifier 'h'
 autoImplicitForbidden.lean:13:24-13:27: error: unknown identifier 'Bla'
 autoImplicitForbidden.lean:16:21-16:24: error: unknown identifier 'Foo'
 autoImplicitForbidden.lean:20:18-20:21: error: unknown identifier 'Ex2'
+autoImplicitForbidden.lean:28:14-28:20: error: unknown identifier 'foobar'
+constructor Bar.mk.{u_1} : ({Na : Sort u_1} → Na) → Nat → Bar