diff --git a/src/Lean/Structure.lean b/src/Lean/Structure.lean
index 4cda828ccb..b69738bead 100644
--- a/src/Lean/Structure.lean
+++ b/src/Lean/Structure.lean
@@ -82,6 +82,15 @@ def getParentStructures (env : Environment) (structName : Name) : Array Name :=
       | some parentStructName => acc.push parentStructName
       | none                  => acc
 
+/-- Return all parent structures -/
+partial def getAllParentStructures (env : Environment) (structName : Name) : Array Name :=
+  visit structName |>.run #[] |>.2
+where
+  visit (structName : Name) : StateT (Array Name) Id Unit := do
+    for p in getParentStructures env structName do
+      modify fun s => s.push p
+      visit p
+
 /-- `findField? env S fname`. If `fname` is defined in a parent `S'` of `S`, return `S'` -/
 partial def findField? (env : Environment) (structName : Name) (fieldName : Name) : Option Name :=
   if (getStructureFields env structName).contains fieldName then
diff --git a/tests/lean/run/structure.lean b/tests/lean/run/structure.lean
index 08da0c3310..2d47702d93 100644
--- a/tests/lean/run/structure.lean
+++ b/tests/lean/run/structure.lean
@@ -24,25 +24,27 @@ inductive D
 | mk (x y z : Nat) : D
 
 def tst : CoreM Unit :=
-do let env ← getEnv;
-   IO.println (getStructureFields env `Lean.Environment);
-   check $ getStructureFields env `S4 == #[`toS2, `toS3, `s];
-   check $ getStructureFields env `S1 == #[`x, `y];
-   check $ isSubobjectField? env `S4 `toS2 == some `S2;
-   check $ getParentStructures env `S4 == #[`S2, `S3];
-   check $ findField? env `S4 `x == some `S1;
-   check $ findField? env `S4 `x1 == none;
-   check $ isStructure env `S1;
-   check $ isStructure env `S2;
-   check $ isStructure env `S3;
-   check $ isStructure env `S4;
-   check $ isStructure env `S5;
-   check $ !isStructure env `Nat;
-   check $ !isStructure env `D;
-   IO.println (getStructureFieldsFlattened env `S4);
-   IO.println (getStructureFields env `D);
-   IO.println (getPathToBaseStructure? env `S1 `S4);
-   check $ getPathToBaseStructure? env `S1 `S4 == some [`S4.toS2, `S2.toS1];
+do let env ← getEnv
+   IO.println (getStructureFields env `Lean.Environment)
+   check $ getStructureFields env `S4 == #[`toS2, `toS3, `s]
+   check $ getStructureFields env `S1 == #[`x, `y]
+   check $ isSubobjectField? env `S4 `toS2 == some `S2
+   check $ getParentStructures env `S4 == #[`S2, `S3]
+   check $ findField? env `S4 `x == some `S1
+   check $ findField? env `S4 `x1 == none
+   check $ isStructure env `S1
+   check $ isStructure env `S2
+   check $ isStructure env `S3
+   check $ isStructure env `S4
+   check $ isStructure env `S5
+   check $ !isStructure env `Nat
+   check $ !isStructure env `D
+   IO.println (getStructureFieldsFlattened env `S4)
+   IO.println (getStructureFields env `D)
+   IO.println (getPathToBaseStructure? env `S1 `S4)
+   IO.println (getParentStructures env `S4)
+   IO.println (getAllParentStructures env `S4)
+   check $ getPathToBaseStructure? env `S1 `S4 == some [`S4.toS2, `S2.toS1]
    pure ()
 
 #eval tst