diff --git a/library/init/meta/decl_cmds.lean b/library/init/meta/decl_cmds.lean
deleted file mode 100644
index 46e7c8e47e..0000000000
--- a/library/init/meta/decl_cmds.lean
+++ /dev/null
@@ -1,50 +0,0 @@
-/-
-Copyright (c) 2016 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import init.meta.tactic init.meta.rb_map
-open tactic
-open native
-private meta def apply_replacement (replacements : name_map name) (e : expr) : expr :=
-e.replace (λ e d,
-  match e with
-  | expr.const n ls :=
-    (match replacements.find n with
-     | some new_n := some (expr.const new_n ls)
-     | none       := none)
-  | _ := none)
-
-/-- Given a set of constant renamings `replacements` and a declaration name `src_decl_name`, create a new
-   declaration called `new_decl_name` s.t. its type is the type of `src_decl_name` after applying the
-   given constant replacement.
-
-   Remark: the new type must be definitionally equal to the type of `src_decl_name`.
-
-   Example:
-   Assume the environment contains
-        def f : nat -> nat  := ...
-        def g : nat -> nat  := f
-        lemma f_lemma : forall a, f a > 0 := ...
-
-   Moreover, assume we have a mapping M containing `f -> `g
-   Then, the command
-        run_command copy_decl_updating_type M `f_lemma `g_lemma
-   creates the declaration
-        lemma g_lemma : forall a, g a > 0 := ... -/
-meta def copy_decl_updating_type (replacements : name_map name) (src_decl_name : name) (new_decl_name : name) : command :=
-do env  ← get_env,
-   decl ← env.get src_decl_name,
-   let decl := decl.update_name $ new_decl_name,
-   let decl := decl.update_type $ apply_replacement replacements decl.type,
-   let decl := decl.update_value $ expr.const src_decl_name (decl.univ_params.map level.param),
-   add_decl decl
-
-meta def copy_decl_using (replacements : name_map name) (src_decl_name : name) (new_decl_name : name) : command :=
-do env      ← get_env,
-   decl     ← env.get src_decl_name,
-   let decl := decl.update_name $ new_decl_name,
-   let decl := decl.update_type $ apply_replacement replacements decl.type,
-   let decl := decl.map_value $ apply_replacement replacements,
-   add_decl decl
diff --git a/library/init/meta/expr.lean b/library/init/meta/expr.lean
index 317887d503..aff782d151 100644
--- a/library/init/meta/expr.lean
+++ b/library/init/meta/expr.lean
@@ -91,13 +91,6 @@ meta constant expr.lex_lt : expr → expr → bool
 meta constant expr.fold {α : Type} : expr → α → (expr → nat → α → α) → α
 meta constant expr.replace : expr → (expr → nat → option expr) → expr
 
-meta constant expr.abstract_local  : expr → name → expr
-meta constant expr.abstract_locals : expr → list name → expr
-
-meta def expr.abstract : expr → expr → expr
-| e (expr.local_const n m bi t) := e.abstract_local n
-| e _                           := e
-
 meta constant expr.instantiate_univ_params : expr → list (name × level) → expr
 meta constant expr.instantiate_var         : expr → expr → expr
 meta constant expr.instantiate_vars        : expr → list expr → expr
@@ -183,12 +176,6 @@ meta constant mk_sorry (type : expr) : expr
 /-- Checks whether e is sorry, and returns its type. -/
 meta constant is_sorry (e : expr) : option expr
 
-meta def instantiate_local (n : name) (s : expr) (e : expr) : expr :=
-instantiate_var (abstract_local e n) s
-
-meta def instantiate_locals (s : list (name × expr)) (e : expr) : expr :=
-instantiate_vars (abstract_locals e (list.reverse (list.map prod.fst s))) (list.map prod.snd s)
-
 meta def is_var : expr → bool
 | (var _) := tt
 | _       := ff
@@ -228,15 +215,6 @@ meta def mk_app : expr → list expr → expr
 | e []      := e
 | e (x::xs) := mk_app (e x) xs
 
-meta def mk_binding (ctor : name → binder_info → expr → expr → expr) (e : expr) : Π (l : expr), expr
-| (local_const n pp_n bi ty) := ctor pp_n bi ty (e.abstract_local n)
-| _                          := e
-
-/-- (bind_pi e l) abstracts and pi-binds the local `l` in `e` -/
-meta def bind_pi := mk_binding pi
-/-- (bind_lambda e l) abstracts and lambda-binds the local `l` in `e` -/
-meta def bind_lambda := mk_binding lam
-
 meta def ith_arg_aux : expr → nat → expr
 | (app f a) 0     := a
 | (app f a) (n+1) := ith_arg_aux f n
@@ -261,14 +239,6 @@ meta def local_uniq_name : expr → name
 | (local_const n m bi t) := n
 | e                      := name.anonymous
 
-meta def local_pp_name : expr elab → name
-| (local_const x n bi t) := n
-| e                      := name.anonymous
-
-meta def local_type : expr elab → expr elab
-| (local_const _ _ _ t) := t
-| e := e
-
 meta def is_aux_decl : expr → bool
 | (local_const _ _ binder_info.aux_decl _) := tt
 | _                                        := ff
diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index 6fe004314e..239e3e8772 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -466,7 +466,9 @@ focus1 $ do {
    rs ← tactic.induction e ids rec_name,
    all_goals $ do {
      intron n,
-     clear_lst (newvars.map local_pp_name),
+     /- TODO: the following command is not reliable since it is based on user facing name.
+        Moreover, we are not storing them anymore on local constants. -/
+     -- clear_lst (newvars.map local_pp_name),
      (e::locals).mfor (try ∘ clear) },
 
    set_induction_tags in_tag rs }
diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index 313780b9ad..c9c628488f 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -312,26 +312,6 @@ meta constant mk_app (fn : name) (args : list expr) (md := semireducible) : tact
    ```
 -/
 meta constant mk_mapp (fn : name) (args : list (option expr)) (md := semireducible) : tactic expr
-/-- (mk_congr_arg h₁ h₂) is a more efficient version of (mk_app `congr_arg [h₁, h₂]) -/
-meta constant mk_congr_arg  : expr → expr → tactic expr
-/-- (mk_congr_fun h₁ h₂) is a more efficient version of (mk_app `congr_fun [h₁, h₂]) -/
-meta constant mk_congr_fun  : expr → expr → tactic expr
-/-- (mk_congr h₁ h₂) is a more efficient version of (mk_app `congr [h₁, h₂]) -/
-meta constant mk_congr      : expr → expr → tactic expr
-/-- (mk_eq_refl h) is a more efficient version of (mk_app `eq.refl [h]) -/
-meta constant mk_eq_refl    : expr → tactic expr
-/-- (mk_eq_symm h) is a more efficient version of (mk_app `eq.symm [h]) -/
-meta constant mk_eq_symm    : expr → tactic expr
-/-- (mk_eq_trans h₁ h₂) is a more efficient version of (mk_app `eq.trans [h₁, h₂]) -/
-meta constant mk_eq_trans   : expr → expr → tactic expr
-/-- (mk_eq_mp h₁ h₂) is a more efficient version of (mk_app `eq.mp [h₁, h₂]) -/
-meta constant mk_eq_mp      : expr → expr → tactic expr
-/-- (mk_eq_mpr h₁ h₂) is a more efficient version of (mk_app `eq.mpr [h₁, h₂]) -/
-meta constant mk_eq_mpr      : expr → expr → tactic expr
-/- Given a local constant t, if t has type (lhs = rhs) apply substitution.
-   Otherwise, try to find a local constant that has type of the form (t = t') or (t' = t).
-   The tactic fails if the given expression is not a local constant. -/
-meta constant subst_core     : expr → tactic unit
 /-- Close the current goal using `e`. Fail is the type of `e` is not definitionally equal to
     the target type. -/
 meta constant exact (e : expr) (md := semireducible) : tactic unit
@@ -636,50 +616,6 @@ meta def clear_lst : list name → tactic unit
 | []      := skip
 | (n::ns) := do H ← get_local n, clear H, clear_lst ns
 
-meta def match_not (e : expr) : tactic expr :=
-match (expr.is_not e) with
-| (some a) := return a
-| none     := fail "expression is not a negation"
-
-meta def match_and (e : expr) : tactic (expr × expr) :=
-match (expr.is_and e) with
-| (some (α, β)) := return (α, β)
-| none     := fail "expression is not a conjunction"
-
-meta def match_or (e : expr) : tactic (expr × expr) :=
-match (expr.is_or e) with
-| (some (α, β)) := return (α, β)
-| none     := fail "expression is not a disjunction"
-
-meta def match_iff (e : expr) : tactic (expr × expr) :=
-match (expr.is_iff e) with
-| (some (lhs, rhs)) := return (lhs, rhs)
-| none              := fail "expression is not an iff"
-
-meta def match_eq (e : expr) : tactic (expr × expr) :=
-match (expr.is_eq e) with
-| (some (lhs, rhs)) := return (lhs, rhs)
-| none              := fail "expression is not an equality"
-
-meta def match_ne (e : expr) : tactic (expr × expr) :=
-match (expr.is_ne e) with
-| (some (lhs, rhs)) := return (lhs, rhs)
-| none              := fail "expression is not a disequality"
-
-meta def match_heq (e : expr) : tactic (expr × expr × expr × expr) :=
-do match (expr.is_heq e) with
-| (some (α, lhs, β, rhs)) := return (α, lhs, β, rhs)
-| none                    := fail "expression is not a heterogeneous equality"
-
-meta def match_refl_app (e : expr) : tactic (name × expr × expr) :=
-do env ← get_env,
-match (environment.is_refl_app env e) with
-| (some (R, lhs, rhs)) := return (R, lhs, rhs)
-| none                 := fail "expression is not an application of a reflexive relation"
-
-meta def match_app_of (e : expr) (n : name) : tactic (list expr) :=
-guard (expr.is_app_of e n) >> return e.get_app_args
-
 meta def get_local_type (n : name) : tactic expr :=
 get_local n >>= infer_type
 
@@ -1004,38 +940,10 @@ return $ expr.mk_sorry t
 meta def admit : tactic unit :=
 target >>= exact ∘ expr.mk_sorry
 
-private meta def get_pi_arity_aux : expr → tactic nat
-| (expr.pi n bi d b) :=
-  do m     ← mk_fresh_name,
-     let l := expr.local_const m n bi d,
-     new_b ← whnf (expr.instantiate_var b l),
-     r     ← get_pi_arity_aux new_b,
-     return (r + 1)
-| e                  := return 0
-
-/-- Compute the arity of the given (Pi-)type -/
-meta def get_pi_arity (type : expr) : tactic nat :=
-whnf type >>= get_pi_arity_aux
-
-/-- Compute the arity of the given function -/
-meta def get_arity (fn : expr) : tactic nat :=
-infer_type fn >>= get_pi_arity
-
 meta def triv : tactic unit := mk_const `trivial >>= exact
 
 notation `dec_trivial` := of_as_true (by tactic.triv)
 
-meta def by_contradiction (H : option name := none) : tactic expr :=
-do tgt : expr ← target,
-   (match_not tgt >> return ())
-   <|>
-   (mk_mapp `decidable.by_contradiction [some tgt, none] >>= eapply >> skip)
-   <|>
-   fail "tactic by_contradiction failed, target is not a negation nor a decidable proposition (remark: when 'local attribute classical.prop_decidable [instance]' is used all propositions are decidable)",
-   match H with
-   | some n := intro n
-   | none   := intro1
-
 private meta def generalizes_aux (md : transparency) : list expr → tactic unit
 | []      := skip
 | (e::es) := generalize e `x md >> generalizes_aux es
@@ -1189,19 +1097,6 @@ do h ← get_local curr,
    intro new,
    intron (n - 1)
 
-/--
-"Replace" hypothesis `h : type` with `h : new_type` where `eq_pr` is a proof
-that (type = new_type). The tactic actually creates a new hypothesis
-with the same user facing name, and (tries to) clear `h`.
-The `clear` step fails if `h` has forward dependencies. In this case, the old `h`
-will remain in the local context. The tactic returns the new hypothesis. -/
-meta def replace_hyp (h : expr) (new_type : expr) (eq_pr : expr) : tactic expr :=
-do h_type ← infer_type h,
-   new_h ← assert h.local_pp_name new_type,
-   mk_eq_mp eq_pr h >>= exact,
-   try $ clear h,
-   return new_h
-
 meta def main_goal : tactic expr :=
 do g::gs ← get_goals, return g
 
@@ -1219,58 +1114,6 @@ main_goal >>= get_tag
 meta def set_main_tag (t : tag) : tactic unit :=
 do g ← main_goal, set_tag g t
 
-meta def subst (h : expr) : tactic unit :=
-(do guard h.is_local_constant,
-    some (α, lhs, β, rhs) ← expr.is_heq <$> infer_type h,
-    is_def_eq α β,
-    new_h_type ← mk_app `eq [lhs, rhs],
-    new_h_pr   ← mk_app `eq_of_heq [h],
-    new_h ← assertv h.local_pp_name new_h_type new_h_pr,
-    try (clear h),
-    subst_core new_h)
-<|> subst_core h
 end tactic
 
 notation [parsing_only] `command`:max := tactic unit
-
-open tactic
-
-namespace list
-
-meta def for_each {α} : list α → (α → tactic unit) → tactic unit
-| []      fn := skip
-| (e::es) fn := do fn e, for_each es fn
-
-meta def any_of {α β} : list α → (α → tactic β) → tactic β
-| []      fn := failed
-| (e::es) fn := do opt_b ← try_core (fn e),
-                   match opt_b with
-                   | some b := return b
-                   | none   := any_of es fn
-end list
-
-/- Install monad laws tactic and use it to prove some instances. -/
-
-meta def order_laws_tac := whnf_target >> intros >> to_expr ``(iff.refl _) >>= exact
-
-meta def monad_from_pure_bind {m : Type u → Type v}
-  (pure : Π {α : Type u}, α → m α)
-  (bind : Π {α β : Type u}, m α → (α → m β) → m β) : monad m :=
-{pure := @pure, bind := @bind}
-
-namespace tactic
-meta def mk_id_proof (prop : expr) (pr : expr) : expr :=
-expr.app (expr.app (expr.const ``id [level.zero]) prop) pr
-
-meta def mk_id_eq (lhs : expr) (rhs : expr) (pr : expr) : tactic expr :=
-do prop ← mk_app `eq [lhs, rhs],
-   return $ mk_id_proof prop pr
-
-meta def replace_target (new_target : expr) (pr : expr) : tactic unit :=
-do t ← target,
-   assert `htarget new_target, swap,
-   ht        ← get_local `htarget,
-   locked_pr ← mk_id_eq t new_target pr,
-   mk_eq_mpr locked_pr ht >>= exact
-
-end tactic