From 203e5f76bdc9effea4ff316a5416108740b6da5f Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 19 Aug 2020 15:01:29 +0200
Subject: [PATCH] fix: bug found by `getArg` panic

---
 src/Lean/Elab/StructInst.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean
index 15c7133fcb..8356f0bc0c 100644
--- a/src/Lean/Elab/StructInst.lean
+++ b/src/Lean/Elab/StructInst.lean
@@ -424,7 +424,7 @@ fields ← fieldNames.foldlM
         | Source.implicit _     => addField (FieldVal.term (mkHole s.ref))
         | Source.explicit stx _ =>
           -- stx is of the form `optional (try (termParser >> "with"))`
-          let src := (stx.getArg 0).getArg 0;
+          let src := stx.getArg 0;
           let val := mkProjStx src fieldName;
           addField (FieldVal.term val))
   [];