From 4c15c9833d66dba261cc43560338a7f05511a859 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 17 Sep 2016 20:04:14 -0700
Subject: [PATCH] fix(frontends/lean/elaborator): use_elim_elab_core

---
 library/init/wf.lean              | 5 +----
 src/frontends/lean/elaborator.cpp | 1 -
 2 files changed, 1 insertion(+), 5 deletions(-)

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);