diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index 08b1e8bfdf..6fcae75d80 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -129,6 +129,8 @@ fieldBinders.foldlM
     idents.foldlM
       (fun (views : Array StructFieldView) ident => do
         let name     := ident.getId;
+        when (isInternalSubobjectFieldName name) $
+          throwError ident ("invalid field name '" ++ name ++ "', identifiers starting with '_' are reserved to the system");
         let declName := structDeclName ++ name;
         declName ← applyVisibility ident modifiers.visibility declName;
         pure $ views.push {
diff --git a/tests/lean/struct1.lean b/tests/lean/struct1.lean
index c13aacafe8..280869c92b 100644
--- a/tests/lean/struct1.lean
+++ b/tests/lean/struct1.lean
@@ -17,3 +17,9 @@ structure S extends A Nat, A Bool := -- error field toA already declared
 
 structure S extends A Nat, B Bool := -- error field `x` from `B` has already been declared
 (x : Nat)
+
+structure S := -- error '_' is not allowed
+(_x : Nat)
+
+structure S := -- error '_' is not allowed
+(x _y : Nat)