diff --git a/library/init/wf.lean b/library/init/wf.lean
index 8eb04ffdda..6f2dfd6b4b 100644
--- a/library/init/wf.lean
+++ b/library/init/wf.lean
@@ -58,10 +58,7 @@ namespace well_founded
 
   theorem fix_F_eq (x : A) (r : acc R x) :
     fix_F F x r = F x (λ (y : A) (p : y ≺ x), fix_F F y (acc.inv r p)) :=
-  @acc.drec A R
-    (λ x r, fix_F F x r = F x (λ (y : A) (p : y ≺ x), fix_F F y (acc.inv r p)))
-    (λ x r ih, rfl)
-    x r
+  acc.drec (λ x r ih, rfl) r
   end
 
   variables {A : Type u} {C : A → Type v} {R : A → A → Prop}
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 7abb8b705d..135a28c8c8 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -327,7 +327,6 @@ auto elaborator::use_elim_elab_core(name const & fn) -> optional<elim_info> {
                 found[*pos] = true;
                 idxs.push_back(i);
             }
-            continue;
         }
 
         expr param_type = m_ctx.infer(param);