fix: disable auto implicits in structure field default values

src/Lean/Elab/Structure.lean

diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index 9a1976b..8496c9d 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -500,7 +500,7 @@
         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 @@
         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

tests/lean/autoImplicitForbidden.lean

diff --git a/tests/lean/autoImplicitForbidden.lean b/tests/lean/autoImplicitForbidden.lean
index 54b54dc..9cc1157 100644
--- a/tests/lean/autoImplicitForbidden.lean
+++ b/tests/lean/autoImplicitForbidden.lean
@@ -21,3 +21,10 @@
 
   inductive Ex2 : Type
 end
+
+
+structure Bar :=
+  (x : Na)
+  (y : Nat := foobar)  -- Error at `foobar`
+
+#print Bar.mk

tests/lean/autoImplicitForbidden.lean.expected.out

diff --git a/tests/lean/autoImplicitForbidden.lean.expected.out b/tests/lean/autoImplicitForbidden.lean.expected.out
index 33c9afc..dc28113 100644
--- a/tests/lean/autoImplicitForbidden.lean.expected.out
+++ b/tests/lean/autoImplicitForbidden.lean.expected.out
@@ -3,3 +3,5 @@
 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