diff --git a/src/Lean/Elab/LetRec.lean b/src/Lean/Elab/LetRec.lean
index fd621c1755..d3d6fcab0b 100644
--- a/src/Lean/Elab/LetRec.lean
+++ b/src/Lean/Elab/LetRec.lean
@@ -79,7 +79,7 @@ private partial def withAuxLocalDecls {α} (views : Array LetRecDeclView) (k : A
   let rec loop (i : Nat) (fvars : Array Expr) : TermElabM α :=
     if h : i < views.size then
       let view := views.get ⟨i, h⟩
-      withLocalDeclD view.shortDeclName view.type fun fvar => loop (i+1) (fvars.push fvar)
+      withLocalDecl view.shortDeclName BinderInfo.auxDecl view.type fun fvar => loop (i+1) (fvars.push fvar)
     else
       k fvars
   loop 0 #[]
diff --git a/tests/lean/letRecMissingAnnotation.lean b/tests/lean/letRecMissingAnnotation.lean
new file mode 100644
index 0000000000..b88696b5fb
--- /dev/null
+++ b/tests/lean/letRecMissingAnnotation.lean
@@ -0,0 +1,8 @@
+def sum (as : Array Nat) : Nat :=
+  let rec go (i : Nat) (s : Nat) : Nat :=
+    if h : i < as.size then
+      go (i+2) (s + as.get ⟨i, h⟩) -- Error
+    else
+      s
+  go 0 0
+termination_by measure (fun ⟨a, i, _⟩ => a.size - i)
diff --git a/tests/lean/letRecMissingAnnotation.lean.expected.out b/tests/lean/letRecMissingAnnotation.lean.expected.out
new file mode 100644
index 0000000000..06403ceb7b
--- /dev/null
+++ b/tests/lean/letRecMissingAnnotation.lean.expected.out
@@ -0,0 +1,5 @@
+letRecMissingAnnotation.lean:4:6-4:34: error: unsolved goals
+as : Array Nat
+i s : Nat
+h : i < Array.size as
+⊢ Array.size as - (i + 2) < Array.size as - i