diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 6b2bf774c9..60df180bde 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -1272,7 +1272,7 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
         LVal.fieldName comp (toString comp.getId) none e
       elabAppFn e (newLVals ++ lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
     let elabFieldIdx (e idxStx : Syntax) := do
-      let idx := idxStx.isFieldIdx?.get!
+      let some idx := idxStx.isFieldIdx? | throwError "invalid field index"
       elabAppFn e (LVal.fieldIdx idxStx idx :: lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
     match f with
     | `($(e).$idx:fieldIdx) => elabFieldIdx e idx
diff --git a/tests/lean/1707.lean b/tests/lean/1707.lean
new file mode 100644
index 0000000000..f34de0b48c
--- /dev/null
+++ b/tests/lean/1707.lean
@@ -0,0 +1 @@
+def y := c.5ÿ
diff --git a/tests/lean/1707.lean.expected.out b/tests/lean/1707.lean.expected.out
new file mode 100644
index 0000000000..09f980e684
--- /dev/null
+++ b/tests/lean/1707.lean.expected.out
@@ -0,0 +1,2 @@
+1707.lean:1:9-1:12: error: invalid field index
+1707.lean:1:12: error: expected command