diff --git a/library/init/data/list/lemmas.lean b/library/init/data/list/lemmas.lean
index fc6eba0a3b..f719451179 100644
--- a/library/init/data/list/lemmas.lean
+++ b/library/init/data/list/lemmas.lean
@@ -234,7 +234,7 @@ lemma mem_or_mem_of_mem_append {a : α} : ∀ {s t : list α}, a ∈ s ++ t →
   end
 
 lemma mem_append_of_mem_or_mem {a : α} {s t : list α} : a ∈ s ∨ a ∈ t → a ∈ s ++ t :=
-list.induction_on s
+list.rec_on s
   (take h, or.elim h false.elim id)
   (take b s,
     assume ih : a ∈ s ∨ a ∈ t → a ∈ s ++ t,
@@ -268,7 +268,7 @@ lemma length_pos_of_mem {a : α} : ∀ {l : list α}, a ∈ l → 0 < length l
 | (b::l) := suppose a ∈ b::l, nat.zero_lt_succ _
 
 lemma mem_split {a : α} {l : list α} : a ∈ l → ∃ s t : list α, l = s ++ (a::t) :=
-list.induction_on l
+list.rec_on l
   (suppose a ∈ [], begin simp at this, contradiction end)
   (take b l,
     assume ih : a ∈ l → ∃ s t : list α, l = s ++ (a::t),
diff --git a/library/init/data/sigma/lex.lean b/library/init/data/sigma/lex.lean
index b01ac062f5..5f8225223d 100644
--- a/library/init/data/sigma/lex.lean
+++ b/library/init/data/sigma/lex.lean
@@ -48,7 +48,7 @@ section
 
   -- The lexicographical order of well founded relations is well-founded
   def lex_wf (ha : well_founded r) (hb : ∀ x, well_founded (s x)) : well_founded (lex r s) :=
-  well_founded.intro (λ p, destruct p (λ a b, lex_accessible (well_founded.apply ha a) hb b))
+  well_founded.intro (λ p, cases_on p (λ a b, lex_accessible (well_founded.apply ha a) hb b))
 end
 
 section
@@ -59,7 +59,7 @@ section
 
   def lex_ndep_wf {r  : α → α → Prop} {s : β → β → Prop} (ha : well_founded r) (hb : well_founded s)
                   : well_founded (lex_ndep r s) :=
-  well_founded.intro (λ p, destruct p (λ a b, lex_accessible (well_founded.apply ha a) (λ x, hb) b))
+  well_founded.intro (λ p, cases_on p (λ a b, lex_accessible (well_founded.apply ha a) (λ x, hb) b))
 end
 
 section
@@ -100,7 +100,7 @@ section
             aux rfl rfl)))
 
   def rev_lex_wf (ha : well_founded r) (hb : well_founded s) : well_founded (rev_lex r s) :=
-  well_founded.intro (λ p, destruct p (λ a b, rev_lex_accessible (apply hb b) (well_founded.apply ha) a))
+  well_founded.intro (λ p, cases_on p (λ a b, rev_lex_accessible (apply hb b) (well_founded.apply ha) a))
 end
 
 section
diff --git a/library/init/wf.lean b/library/init/wf.lean
index 7b6c4fafd8..39a7592554 100644
--- a/library/init/wf.lean
+++ b/library/init/wf.lean
@@ -172,7 +172,7 @@ section
 
   -- The lexicographical order of well founded relations is well-founded
   def lex_wf (ha : well_founded ra) (hb : well_founded rb) : well_founded (lex ra rb) :=
-  ⟨λ p, destruct p (λ a b, lex_accessible (apply ha a) (well_founded.apply hb) b)⟩
+  ⟨λ p, cases_on p (λ a b, lex_accessible (apply ha a) (well_founded.apply hb) b)⟩
 
   -- relational product is a subrelation of the lex
   def rprod_sub_lex : ∀ a b, rprod ra rb a b → lex ra rb a b :=
diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp
index 182346d160..64a509dda4 100644
--- a/src/frontends/lean/structure_cmd.cpp
+++ b/src/frontends/lean/structure_cmd.cpp
@@ -42,7 +42,6 @@ Author: Leonardo de Moura
 #include "library/documentation.h"
 #include "library/compiler/vm_compiler.h"
 #include "library/constructions/rec_on.h"
-#include "library/constructions/induction_on.h"
 #include "library/constructions/cases_on.h"
 #include "library/constructions/projection.h"
 #include "library/constructions/no_confusion.h"
@@ -972,10 +971,6 @@ struct structure_cmd_fn {
         name rec_on_name(m_name, "rec_on");
         add_rec_alias(rec_on_name);
         m_env = add_aux_recursor(m_env, rec_on_name);
-        m_env = mk_induction_on(m_env, m_name);
-        name induction_on_name(m_name, "induction_on");
-        add_alias(induction_on_name);
-        add_rec_on_alias(name(m_name, "destruct"));
         name cases_on_name(m_name, "cases_on");
         add_rec_on_alias(cases_on_name);
         m_env = add_aux_recursor(m_env, cases_on_name);
@@ -1080,7 +1075,6 @@ struct structure_cmd_fn {
             return;
         if (!has_and_decls(m_env))
             return;
-
         m_env = mk_injective_lemmas(m_env, m_name);
         add_alias(mk_injective_name(m_name));
         add_alias(mk_injective_arrow_name(m_name));
diff --git a/src/library/constructions/CMakeLists.txt b/src/library/constructions/CMakeLists.txt
index a6aa07ecfb..b36d988a9a 100644
--- a/src/library/constructions/CMakeLists.txt
+++ b/src/library/constructions/CMakeLists.txt
@@ -1,3 +1,3 @@
-add_library(constructions OBJECT rec_on.cpp induction_on.cpp cases_on.cpp
+add_library(constructions OBJECT rec_on.cpp cases_on.cpp
   no_confusion.cpp projection.cpp brec_on.cpp init_module.cpp has_sizeof.cpp
   constructor.cpp drec.cpp injective.cpp)
diff --git a/src/library/constructions/induction_on.cpp b/src/library/constructions/induction_on.cpp
deleted file mode 100644
index 6663aeb541..0000000000
--- a/src/library/constructions/induction_on.cpp
+++ /dev/null
@@ -1,50 +0,0 @@
-/*
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "util/sstream.h"
-#include "kernel/environment.h"
-#include "kernel/instantiate.h"
-#include "kernel/type_checker.h"
-#include "library/module.h"
-#include "library/protected.h"
-#include "library/util.h"
-#include "library/aux_recursors.h"
-
-namespace lean {
-environment mk_induction_on(environment const & env, name const & n) {
-    if (!inductive::is_inductive_decl(env, n))
-        throw exception(sstream() << "error in 'induction_on' generation, '" << n << "' is not an inductive datatype");
-    name rec_on_name(n, "rec_on");
-    name induction_on_name(n, "induction_on");
-    declaration rec_on_decl   = env.get(rec_on_name);
-    declaration ind_decl      = env.get(n);
-    unsigned rec_on_num_univs = rec_on_decl.get_num_univ_params();
-    unsigned ind_num_univs    = ind_decl.get_num_univ_params();
-    environment new_env       = env;
-    if (rec_on_num_univs == ind_num_univs) {
-        // easy case, induction_on is just an alias for rec_on
-        certified_declaration cdecl = check(new_env,
-                                            mk_definition_inferring_trusted(new_env, induction_on_name, rec_on_decl.get_univ_params(),
-                                                                            rec_on_decl.get_type(), rec_on_decl.get_value(),
-                                                                            reducibility_hints::mk_opaque()));
-        new_env = add_aux_recursor(new_env, induction_on_name);
-        new_env = module::add(new_env, cdecl);
-    } else {
-        level_param_names induction_on_univs = tail(rec_on_decl.get_univ_params());
-        name              from  = head(rec_on_decl.get_univ_params());
-        level             to    = mk_level_zero();
-        expr induction_on_type  = instantiate_univ_param(rec_on_decl.get_type(), from, to);
-        expr induction_on_value = instantiate_univ_param(rec_on_decl.get_value(), from, to);
-        certified_declaration cdecl = check(new_env,
-                                            mk_definition_inferring_trusted(new_env, induction_on_name, induction_on_univs,
-                                                                            induction_on_type, induction_on_value,
-                                                                            reducibility_hints::mk_opaque()));
-        new_env = add_aux_recursor(new_env, induction_on_name);
-        new_env = module::add(new_env, cdecl);
-    }
-    return add_protected(new_env, induction_on_name);
-}
-}
diff --git a/src/library/constructions/induction_on.h b/src/library/constructions/induction_on.h
deleted file mode 100644
index e67881ebd2..0000000000
--- a/src/library/constructions/induction_on.h
+++ /dev/null
@@ -1,19 +0,0 @@
-/*
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "kernel/environment.h"
-
-namespace lean {
-/** \brief Given an inductive datatype \c n in \c env, add
-    <tt>n.induction_on</tt> to the environment.
-
-    \remark Throws an exception if \c n is not an inductive datatype.
-
-    \remark Throws an exception if <tt>n.rec_on</tt> is not defined in the given environment.
-*/
-environment mk_induction_on(environment const & env, name const & n);
-}
diff --git a/src/library/inductive_compiler/basic.cpp b/src/library/inductive_compiler/basic.cpp
index 72958ed72e..c208ebced5 100644
--- a/src/library/inductive_compiler/basic.cpp
+++ b/src/library/inductive_compiler/basic.cpp
@@ -16,7 +16,6 @@ Author: Daniel Selsam
 #include "library/inductive_compiler/util.h"
 #include "library/constructions/drec.h"
 #include "library/constructions/rec_on.h"
-#include "library/constructions/induction_on.h"
 #include "library/constructions/cases_on.h"
 #include "library/constructions/brec_on.h"
 #include "library/constructions/no_confusion.h"
@@ -91,9 +90,6 @@ class add_basic_inductive_decl_fn {
         if (gen_rec_on)
             m_env = mk_rec_on(m_env, ind_name);
 
-        if (gen_rec_on)
-            m_env = mk_induction_on(m_env, ind_name);
-
         if (has_unit) {
             if (gen_cases_on)
                 m_env = mk_cases_on(m_env, ind_name);