diff --git a/library/init/meta/expr.lean b/library/init/meta/expr.lean
index 2cd97e2867..2efb6c89f4 100644
--- a/library/init/meta/expr.lean
+++ b/library/init/meta/expr.lean
@@ -89,32 +89,11 @@ meta constant expr.lt : expr → expr → bool
 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.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
 
 protected meta constant expr.subst : expr elab → expr elab → expr elab
 
 /-- `has_var e` returns true iff e has free variables. -/
 meta constant expr.has_bvar_idx   : expr → nat → bool
-meta constant expr.has_meta_var  : expr → bool
-/-- `lower_vars e s d` lowers the free variables >= s in `e` by `d`. That is, a free variable `var i` s.t.
-   `i >= s` is mapped to `var (i-d)`. -/
-meta constant expr.lower_vars    : expr → nat → nat → expr
-/-- Lifts free variables. See `expr.lower_vars` for details. -/
-meta constant expr.lift_vars     : expr → nat → nat → expr
-protected meta constant expr.pos : expr elab → option pos
-/-- `copy_pos_info src tgt` copies position information from `src` to `tgt`. -/
-meta constant expr.copy_pos_info : expr → expr → expr
-
-meta constant expr.is_internal_cnstr : expr → option uint32
-meta constant expr.get_nat_value : expr → option nat
-
-meta constant expr.collect_univ_params : expr → list name
-/-- `occurs e t` returns `tt` iff `e` occurs in `t` -/
-meta constant expr.occurs        : expr → expr → bool
 
 /-- (reflected a) is a special opaque container for a closed `expr` representing `a`.
     It can only be obtained via type class inference, which will use the representation
diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index 306c83c271..4e8609cbbb 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -246,15 +246,7 @@ meta def change (q : parse texpr) : parse (tk "with" *> texpr)? → parse locati
 | none (loc.ns [none]) := do e ← i_to_expr q, change_core e none
 | none (loc.ns [some h]) := do eq ← i_to_expr q, eh ← get_local h, change_core eq (some eh)
 | none _ := fail "change-at does not support multiple locations"
-| (some w) l :=
-  do u ← mk_meta_univ,
-     ty ← mk_meta_var (sort u),
-     eq ← i_to_expr ``(%%q : %%ty),
-     ew ← i_to_expr ``(%%w : %%ty),
-     let repl := λe : expr, e.replace (λ a n, if a = eq then some ew else none),
-     l.try_apply
-       (λh, do e ← infer_type h, change_core (repl e) (some h))
-       (do g ← target, change_core (repl g) none)
+| (some w) l := fail "not implemented yet"
 
 /--
 This tactic provides an exact proof term to solve the main goal. If `t` is the goal and `p` is a term of type `u` then `exact p` succeeds if and only if `t` and `u` can be unified.
@@ -347,28 +339,6 @@ private meta def generalize_arg_p_aux : pexpr → parser (pexpr × name)
 private meta def generalize_arg_p : parser (pexpr × name) :=
 with_desc "expr = id" $ parser.pexpr 0 >>= generalize_arg_p_aux
 
-/--
-`generalize : e = x` replaces all occurrences of `e` in the target with a new hypothesis `x` of the same type.
-
-`generalize h : e = x` in addition registers the hypothesis `h : e = x`.
--/
-meta def generalize (h : parse ident?) (_ : parse $ tk ":") (p : parse generalize_arg_p) : tactic unit :=
-propagate_tags $
-do let (p, x) := p,
-   e ← i_to_expr p,
-   some h ← pure h | tactic.generalize e x >> intro1 >> skip,
-   tgt ← target,
-   -- if generalizing fails, fall back to not replacing anything
-   tgt' ← do {
-     ⟨tgt', _⟩ ← solve_aux tgt (tactic.generalize e x >> target),
-     to_expr ``(Π x, %%e = x → %%(tgt'.binding_body.lift_vars 0 1))
-   } <|> to_expr ``(Π x, %%e = x → %%tgt),
-   t ← assert h tgt',
-   swap,
-   exact ``(%%t %%e rfl),
-   intro x,
-   intro h
-
 meta def cases_arg_p : parser (option name × pexpr) :=
 with_desc "(id :)? expr" $ do
   t ← texpr,
@@ -413,9 +383,6 @@ For example, given `n : nat` and a goal with a hypothesis `h : P n` and target `
 
 `induction e using r` allows the user to specify the principle of induction that should be used. Here `r` should be a theorem whose result type must be of the form `C t`, where `C` is a bound variable and `t` is a (possibly empty) sequence of bound variables
 
-`induction e generalizing z₁ ... zₙ`, where `z₁ ... zₙ` are variables in the local context, generalizes over `z₁ ... zₙ` before applying the induction but then introduces them in each goal. In other words, the net effect is that each inductive hypothesis is generalized.
-
-`induction h : t` will introduce an equality of the form `h : t = C x y`, asserting that the input term is equal to the current constructor case, to the context.
 -/
 meta def induction (hp : parse cases_arg_p) (rec_name : parse using_ident) (ids : parse with_ident_list)
   (revert : parse $ (tk "generalizing" *> ident*)?) : tactic unit :=
@@ -423,10 +390,7 @@ do in_tag ← get_main_tag,
 focus1 $ do {
     -- process `h : t` case
     e ← (match hp with
-         | (some h, p) := do
-           x ← get_unused_name,
-           generalize h () (p, x),
-           get_local x
+         | (some h, p) := fail "not implemented yet"
          | (none, p) := i_to_expr p),
    -- generalize major premise
    e ← if e.is_fvar then pure e
@@ -517,7 +481,7 @@ match pre with
      find_tagged_goal_aux pre
 
 private meta def find_case (goals : list expr) (ty : name) (idx : nat) (num_indices : nat) : option expr → expr → option (expr × expr)
-| case e := if e.has_meta_var then match e with
+| case e := match e with
   | (mvar _ _ _)    :=
     do case ← case,
        guard $ e ∈ goals,
@@ -547,7 +511,6 @@ private meta def find_case (goals : list expr) (ty : name) (idx : nat) (num_indi
   | (lam _ _ _ e) := find_case case e
   | (macro n args) := list.foldl (<|>) none $ args.map (find_case case)
   | _             := none
-  else none
 
 private meta def rename_lams : expr → list name → tactic unit
 | (lam n _ _ e) (n'::ns) := (rename n n' >> rename_lams e ns) <|> rename_lams e (n'::ns)
@@ -630,11 +593,7 @@ meta def cases : parse cases_arg_p → parse with_ident_list → tactic unit
 | (none,   p) ids := do
   e ← i_to_expr p,
   cases_core e ids
-| (some h, p) ids := do
-  x   ← get_unused_name,
-  generalize h () (p, x),
-  hx  ← get_local x,
-  cases_core hx ids
+| (some h, p) ids := fail "not implemented yet"
 
 private meta def try_cases_for_types (type_names : list name) (at_most_one : bool) : tactic unit :=
 any_hyp $ λ h, do
diff --git a/src/library/vm/vm_expr.cpp b/src/library/vm/vm_expr.cpp
index cf7a26ff31..7360f7c2c5 100644
--- a/src/library/vm/vm_expr.cpp
+++ b/src/library/vm/vm_expr.cpp
@@ -238,59 +238,6 @@ vm_obj expr_fold(vm_obj const &, vm_obj const & e, vm_obj const & a, vm_obj cons
     return r;
 }
 
-vm_obj expr_replace(vm_obj const & e, vm_obj const & fn) {
-    expr r = replace(to_expr(e), [&](expr const & o, unsigned d) {
-            vm_obj new_o = invoke(fn, to_obj(o), mk_vm_nat(d));
-            if (is_none(new_o))
-                return none_expr();
-            else
-                return some_expr(to_expr(get_some_value(new_o)));
-        });
-    return to_obj(r);
-}
-
-vm_obj expr_instantiate_univ_params(vm_obj const & e, vm_obj const & nls) {
-    names ns = to_obj_list<name>(nls, [](vm_obj const & p) {
-            lean_assert(csize(p) == 2);
-            return to_name(cfield(p, 0));
-        } );
-    levels ls = to_obj_list<level>(nls, [](vm_obj const & p) {
-            lean_assert(csize(p) == 2);
-            return to_level(cfield(p, 1));
-        } );
-    return to_obj(instantiate_univ_params(to_expr(e), ns, ls));
-}
-
-vm_obj expr_instantiate_var(vm_obj const & e, vm_obj const & v) {
-    return to_obj(instantiate(to_expr(e), to_expr(v)));
-}
-
-vm_obj expr_instantiate_vars(vm_obj const & e, vm_obj const & vs) {
-    buffer<expr> vs_buf;
-    to_buffer_expr(vs, vs_buf);
-    return to_obj(instantiate(to_expr(e), vs_buf.size(), vs_buf.data()));
-}
-
-vm_obj expr_abstract_local(vm_obj const & e, vm_obj const & n) {
-    return to_obj(abstract_local(to_expr(e), to_name(n)));
-}
-
-static void list_name_to_buffer_local(vm_obj const & o, buffer<expr> & r) {
-    if (is_simple(o)) {
-        return;
-    } else {
-        expr dummy = mk_Prop();
-        r.push_back(mk_local(to_name(cfield(o, 0)), dummy));
-        list_name_to_buffer_local(cfield(o, 1), r);
-    }
-}
-
-vm_obj expr_abstract_locals(vm_obj const & e, vm_obj const & ns) {
-    buffer<expr> locals;
-    list_name_to_buffer_local(ns, locals);
-    return to_obj(abstract_locals(to_expr(e), locals.size(), locals.data()));
-}
-
 vm_obj expr_has_bvar_idx(vm_obj const & e, vm_obj const & u) {
     if (auto n = try_to_unsigned(u)) {
         return mk_vm_bool(has_free_var(to_expr(e), *n));
@@ -299,70 +246,11 @@ vm_obj expr_has_bvar_idx(vm_obj const & e, vm_obj const & u) {
     }
 }
 
-vm_obj expr_has_meta_var(vm_obj const & e) {
-    return mk_vm_bool(has_metavar(to_expr(e)));
-}
-
-vm_obj expr_lift_vars(vm_obj const & e, vm_obj const & n1, vm_obj const & n2) {
-    auto u1 = try_to_unsigned(n1);
-    auto u2 = try_to_unsigned(n2);
-    if (u1 && u2)
-        return to_obj(lift_free_vars(to_expr(e), *u1, *u2));
-    else
-        return e;
-}
-
-vm_obj expr_lower_vars(vm_obj const & e, vm_obj const & n1, vm_obj const & n2) {
-    auto u1 = try_to_unsigned(n1);
-    auto u2 = try_to_unsigned(n2);
-    if (u1 && u2)
-        return to_obj(lower_free_vars(to_expr(e), *u1, *u2));
-    else
-        return e;
-}
-
 vm_obj expr_hash(vm_obj const & e) {
     unsigned r = to_expr(e).hash() % LEAN_VM_MAX_SMALL_NAT;
     return mk_vm_simple(r); // make sure it is a simple value
 }
 
-vm_obj expr_copy_pos_info(vm_obj const & src, vm_obj const & tgt) {
-    return to_obj(copy_tag(to_expr(src), copy(to_expr(tgt))));
-}
-
-vm_obj expr_is_internal_cnstr(vm_obj const & e) {
-    auto opt_unsigned = is_internal_cnstr(to_expr(e));
-    if (opt_unsigned) {
-        std::cout << *opt_unsigned << std::endl;
-        vm_obj u = to_obj(*opt_unsigned);
-        return mk_vm_constructor(1, { u });
-    } else {
-        return mk_vm_constructor(0, {});
-    }
-}
-
-vm_obj expr_is_internal_proj(vm_obj const & e) {
-    auto opt_unsigned = is_internal_proj(to_expr(e));
-    if (opt_unsigned) {
-        std::cout << *opt_unsigned << std::endl;
-        vm_obj u = to_obj(*opt_unsigned);
-        return mk_vm_constructor(1, { u });
-    } else {
-        return mk_vm_constructor(0, {});
-    }
-}
-
-vm_obj expr_is_internal_cases(vm_obj const & e) {
-    auto opt_unsigned = is_internal_cases(to_expr(e));
-    if (opt_unsigned) {
-        std::cout << *opt_unsigned << std::endl;
-        vm_obj u = to_obj(*opt_unsigned);
-        return mk_vm_constructor(1, { u });
-    } else {
-        return mk_vm_constructor(0, {});
-    }
-}
-
 vm_obj expr_get_nat_value(vm_obj const & o) {
     expr e = to_expr(o);
     if (is_nat_value(e)) {
@@ -405,10 +293,6 @@ vm_obj vm_mk_string_val_ne_proof(vm_obj const & a, vm_obj const & b) {
     return to_obj(mk_string_val_ne_proof(to_expr(a), to_expr(b)));
 }
 
-vm_obj expr_occurs(vm_obj const & e1, vm_obj const & e2) {
-    return mk_vm_bool(occurs(to_expr(e1), to_expr(e2)));
-}
-
 vm_obj expr_subst(vm_obj const &, vm_obj const & _e1, vm_obj const & _e2) {
     expr const & e1 = to_expr(_e1);
     expr const & e2 = to_expr(_e2);
@@ -439,18 +323,12 @@ vm_obj reflect_string(vm_obj const & s) {
     return to_obj(from_string(to_string(s)));
 }
 
-vm_obj expr_pos(vm_obj const &, vm_obj const & e) {
-    if (auto p = get_pos_info(to_expr(e)))
-        return mk_vm_some(to_obj(*p));
-    return mk_vm_none();
-}
-
 void initialize_vm_expr() {
     DECLARE_VM_BUILTIN(name({"expr", "var"}),              expr_var_intro);
+    DECLARE_VM_BUILTIN(name({"expr", "fvar"}),             expr_local_const_intro);
     DECLARE_VM_BUILTIN(name({"expr", "sort"}),             expr_sort_intro);
     DECLARE_VM_BUILTIN(name({"expr", "const"}),            expr_const_intro);
     DECLARE_VM_BUILTIN(name({"expr", "mvar"}),             expr_mvar_intro);
-    DECLARE_VM_BUILTIN(name({"expr", "local_const"}),      expr_local_const_intro);
     DECLARE_VM_BUILTIN(name({"expr", "app"}),              expr_app_intro);
     DECLARE_VM_BUILTIN(name({"expr", "lam"}),              expr_lam_intro);
     DECLARE_VM_BUILTIN(name({"expr", "pi"}),               expr_pi_intro);
@@ -463,22 +341,9 @@ void initialize_vm_expr() {
     DECLARE_VM_BUILTIN(name({"expr", "lt"}),               expr_lt);
     DECLARE_VM_BUILTIN(name({"expr", "lex_lt"}),           expr_lex_lt);
     DECLARE_VM_BUILTIN(name({"expr", "fold"}),             expr_fold);
-    DECLARE_VM_BUILTIN(name({"expr", "replace"}),          expr_replace);
-    DECLARE_VM_BUILTIN(name({"expr", "instantiate_univ_params"}), expr_instantiate_univ_params);
-    DECLARE_VM_BUILTIN(name({"expr", "instantiate_var"}),  expr_instantiate_var);
-    DECLARE_VM_BUILTIN(name({"expr", "instantiate_vars"}), expr_instantiate_vars);
     DECLARE_VM_BUILTIN(name({"expr", "subst"}),            expr_subst);
-    DECLARE_VM_BUILTIN(name({"expr", "abstract_local"}),   expr_abstract_local);
-    DECLARE_VM_BUILTIN(name({"expr", "abstract_locals"}),  expr_abstract_locals);
     DECLARE_VM_BUILTIN(name({"expr", "has_bvar_idx"}),     expr_has_bvar_idx);
-    DECLARE_VM_BUILTIN(name({"expr", "has_meta_var"}),     expr_has_meta_var);
-    DECLARE_VM_BUILTIN(name({"expr", "lift_vars"}),        expr_lift_vars);
-    DECLARE_VM_BUILTIN(name({"expr", "lower_vars"}),       expr_lower_vars);
     DECLARE_VM_BUILTIN(name({"expr", "hash"}),             expr_hash);
-    DECLARE_VM_BUILTIN(name({"expr", "pos"}),              expr_pos);
-    DECLARE_VM_BUILTIN(name({"expr", "copy_pos_info"}),    expr_copy_pos_info);
-    DECLARE_VM_BUILTIN(name({"expr", "occurs"}),           expr_occurs);
-    DECLARE_VM_BUILTIN(name({"expr", "collect_univ_params"}), expr_collect_univ_params);
 
     DECLARE_VM_CASES_BUILTIN(name({"expr", "cases_on"}),   expr_cases_on);
 
@@ -493,10 +358,6 @@ void initialize_vm_expr() {
     DECLARE_VM_BUILTIN(name("mk_string_val_ne_proof"),     vm_mk_string_val_ne_proof);
 
     DECLARE_VM_BUILTIN(name("expr", "is_annotation"),      expr_is_annotation);
-
-    // Not sure if we should expose these or what?
-    DECLARE_VM_BUILTIN(name({"expr", "is_internal_cnstr"}), expr_is_internal_cnstr);
-    DECLARE_VM_BUILTIN(name({"expr", "get_nat_value"}), expr_get_nat_value);
 }
 
 void finalize_vm_expr() {