diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index ffee34fa50..dbef2064da 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -442,10 +442,7 @@ private def addCtorFields (fieldInfos : Array StructFieldInfo) : Nat → Expr 
     | StructFieldKind.fromParent =>
       let val := decl.value
       addCtorFields fieldInfos i (type.instantiate1 val)
-    | StructFieldKind.subobject =>
-      let n := mkInternalSubobjectFieldName decl.userName
-      addCtorFields fieldInfos i (mkForall n decl.binderInfo decl.type type)
-    | StructFieldKind.newField =>
+    | _  =>
       addCtorFields fieldInfos i (mkForall decl.userName decl.binderInfo decl.type type)
 
 private def mkCtor (view : StructView) (levelParams : List Name) (params : Array Expr) (fieldInfos : Array StructFieldInfo) : TermElabM Constructor :=
diff --git a/src/Lean/Structure.lean b/src/Lean/Structure.lean
index 79ee7ad468..e03bc92fed 100644
--- a/src/Lean/Structure.lean
+++ b/src/Lean/Structure.lean
@@ -57,10 +57,6 @@ def getStructureInfo? (env : Environment) (structName : Name) : Option Structure
   | some modIdx => structureExt.getModuleEntries env modIdx |>.binSearch { structName } StructureInfo.lt
   | none        => structureExt.getState env |>.map.find? structName
 
-/-- We mark subobject fields by prefixing them with "_" in the structure's intro rule. -/
-def mkInternalSubobjectFieldName (fieldName : Name) : Name :=
-  fieldName.appendBefore "_"
-
 def getStructureCtor (env : Environment) (constName : Name) : ConstructorVal :=
   match env.find? constName with
   | some (ConstantInfo.inductInfo { isRec := false, ctors := [ctorName], .. }) =>