diff --git a/library/init/data/nat/lemmas.lean b/library/init/data/nat/lemmas.lean
index e7587b68c6..b221dc77a4 100644
--- a/library/init/data/nat/lemmas.lean
+++ b/library/init/data/nat/lemmas.lean
@@ -41,7 +41,7 @@ protected lemma add_left_comm : ∀ (n m k : ℕ), n + (m + k) = m + (n + k) :=
 left_comm nat.add nat.add_comm nat.add_assoc
 
 protected lemma add_left_cancel : ∀ {n m k : ℕ}, n + m = n + k → m = k
-| 0        m k := by ctx_simp [nat.zero_add]
+| 0        m k := by simp [nat.zero_add] {contextual := tt}
 | (succ n) m k := λ h,
   have n+m = n+k, begin simp [succ_add] at h, injection h, assumption end,
   add_left_cancel this
@@ -64,7 +64,7 @@ protected lemma zero_ne_one : 0 ≠ (1 : ℕ) :=
 assume h, nat.no_confusion h
 
 lemma eq_zero_of_add_eq_zero_right : ∀ {n m : ℕ}, n + m = 0 → n = 0
-| 0     m := by ctx_simp [nat.zero_add]
+| 0     m := by simp [nat.zero_add] {contextual := tt}
 | (n+1) m := λ h,
   begin
     exfalso,
diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index d0fcf26413..fad6306570 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -481,25 +481,21 @@ It has many variants.
 
 - `simp with attr` simplifies the main goal target using the lemmas tagged with the attribute `[attr]`.
 -/
-meta def simp (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) (loc : parse location) : tactic unit :=
-simp_core {} [] hs attr_names ids loc
-
-/--
-Similar to the `simp` tactic, but uses contextual simplification. For example, when simplifying `t = s → p`,
-the equation `t = s` is automatically added to the set of simplification rules when simplifying `p`.
--/
-meta def ctx_simp (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) (loc : parse location) : tactic unit :=
-simp_core {contextual := tt} [] hs attr_names ids loc
+meta def simp (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) (loc : parse location)
+              (cfg : simplify_config := {}) : tactic unit :=
+simp_core cfg [] hs attr_names ids loc
 
 /--
 Similar to the `simp` tactic, but adds all applicable hypotheses as simplification rules.
 -/
-meta def simp_using_hs (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) : tactic unit :=
+meta def simp_using_hs (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list)
+                       (cfg : simplify_config := {}) : tactic unit :=
 do ctx ← collect_ctx_simps,
-   simp_core {} ctx hs attr_names ids []
+   simp_core cfg ctx hs attr_names ids []
 
-meta def simph (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) : tactic unit :=
-simp_using_hs hs attr_names ids
+meta def simph (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list)
+               (cfg : simplify_config := {}) : tactic unit :=
+simp_using_hs hs attr_names ids cfg
 
 private meta def dsimp_hyps (s : simp_lemmas) : list name → tactic unit
 | []      := skip
@@ -579,12 +575,12 @@ private meta def dunfold_hyps_occs : name → occurrences → list name → tact
 | c occs []  := skip
 | c occs (h::hs) := get_local h >>= dunfold_core_at occs [c] >> dunfold_hyps_occs c occs hs
 
-meta def dunfold_occs : parse ident → list nat → parse location → tactic unit
-| c ps [] := do new_c ← to_qualified_name c, tactic.dunfold_occs_of ps new_c
-| c ps hs := do new_c ← to_qualified_name c, dunfold_hyps_occs new_c (occurrences.pos ps) hs
+meta def dunfold_occs : parse ident → parse location → list nat → tactic unit
+| c [] ps := do new_c ← to_qualified_name c, tactic.dunfold_occs_of ps new_c
+| c hs ps := do new_c ← to_qualified_name c, dunfold_hyps_occs new_c (occurrences.pos ps) hs
 
 /- TODO(Leo): add support for non-refl lemmas -/
-meta def unfold_occs : parse ident → list nat → parse location → tactic unit :=
+meta def unfold_occs : parse ident → parse location → list nat → tactic unit :=
 dunfold_occs
 
 private meta def delta_hyps : list name → list name → tactic unit
diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean
index 8371d082e3..a8242bc8a6 100644
--- a/library/init/meta/simp_tactic.lean
+++ b/library/init/meta/simp_tactic.lean
@@ -192,6 +192,7 @@ structure simplify_config :=
 (canonize_instances : bool := tt)
 (canonize_proofs : bool    := ff)
 (use_axioms : bool         := tt)
+(zeta : bool               := tt)
 
 meta constant simplify_core
   (c : simplify_config)
diff --git a/library/init/meta/smt/interactive.lean b/library/init/meta/smt/interactive.lean
index b5c48d988c..b6569df7a4 100644
--- a/library/init/meta/smt/interactive.lean
+++ b/library/init/meta/smt/interactive.lean
@@ -229,16 +229,18 @@ smt_tactic.all_goals t
 meta def induction (p : parse texpr) (rec_name : parse using_ident) (ids : parse with_ident_list) : smt_tactic unit :=
 slift (tactic.interactive.induction p rec_name ids)
 
-/-- Simplify the target type of the main goal. -/
-meta def simp (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) : smt_tactic unit :=
-tactic.interactive.simp hs attr_names ids []
+open tactic
 
-meta def ctx_simp (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) : smt_tactic unit :=
-tactic.interactive.ctx_simp hs attr_names ids []
+/-- Simplify the target type of the main goal. -/
+meta def simp (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) (cfg : simplify_config := {}) : smt_tactic unit :=
+tactic.interactive.simp hs attr_names ids [] cfg
 
 /-- Simplify the target type of the main goal using simplification lemmas and the current set of hypotheses. -/
-meta def simp_using_hs (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) : smt_tactic unit :=
-tactic.interactive.simp_using_hs hs attr_names ids
+meta def simp_using_hs (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) (cfg : simplify_config := {}) : smt_tactic unit :=
+tactic.interactive.simp_using_hs hs attr_names ids cfg
+
+meta def simph (hs : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) (cfg : simplify_config := {}) : smt_tactic unit :=
+simp_using_hs hs attr_names ids cfg
 
 meta def dsimp (es : parse opt_qexpr_list) (attr_names : parse with_ident_list) (ids : parse without_ident_list) : smt_tactic unit :=
 tactic.interactive.dsimp es attr_names ids []
diff --git a/src/frontends/lean/tactic_notation.cpp b/src/frontends/lean/tactic_notation.cpp
index a1b06f5eed..719a053d36 100644
--- a/src/frontends/lean/tactic_notation.cpp
+++ b/src/frontends/lean/tactic_notation.cpp
@@ -173,11 +173,14 @@ static expr parse_auto_quote_tactic(parser & p, name const & decl_name, name con
             } else if (is_constant(arg_type, irtactic)) {
                 args.push_back(parse_nested_auto_quote_tactic(p, tac_class, use_rstep, report_error));
             } else {
-                args.push_back(p.parse_expr(get_max_prec()));
+                break;
             }
         }
         type = binding_body(type);
     }
+    while (p.curr_lbp() >= get_max_prec()) {
+        args.push_back(p.parse_expr(get_max_prec()));
+    }
     expr r = p.mk_app(p.save_pos(mk_constant(decl_name), pos), args, pos);
     return mk_tactic_step(p, r, pos, tac_class, use_rstep, report_error);
 }
diff --git a/src/frontends/lean/token_table.h b/src/frontends/lean/token_table.h
index 0508c7d2ac..328bb4cf1a 100644
--- a/src/frontends/lean/token_table.h
+++ b/src/frontends/lean/token_table.h
@@ -17,7 +17,7 @@ Author: Leonardo de Moura
 namespace lean {
 // User-level maximum precedence
 unsigned get_max_prec();
-// Internal maximum precedence used for @@, @ and ! operators
+// Internal maximum precedence used for @@ and @ operators
 unsigned get_Max_prec();
 unsigned get_arrow_prec();
 class token_info {
diff --git a/src/library/inductive_compiler/nested.cpp b/src/library/inductive_compiler/nested.cpp
index 2ce80ae8e3..13510d4c2c 100644
--- a/src/library/inductive_compiler/nested.cpp
+++ b/src/library/inductive_compiler/nested.cpp
@@ -1260,16 +1260,17 @@ class add_nested_inductive_decl_fn {
             all_lemmas = add(tctx_whnf, all_lemmas, mlocal_name(H), H_type, H, LEAN_DEFAULT_PRIORITY);
         }
         lean_trace(name({"inductive_compiler", "nested", "simp", "start"}), tout() << thm << "\n";);
-        unsigned max_steps      = 1000000;
-        bool contextual         = false;
-        bool lift_eq            = false;
-        bool canonize_instances = false;
-        bool canonize_proofs    = false;
-        bool use_axioms         = false;
+        simplify_config cfg;
+        cfg.m_max_steps          = 1000000;
+        cfg.m_contextual         = false;
+        cfg.m_lift_eq            = false;
+        cfg.m_canonize_instances = false;
+        cfg.m_canonize_proofs    = false;
+        cfg.m_use_axioms         = false;
+        cfg.m_zeta               = false;
+        cfg.m_use_matcher        = false;
         defeq_can_state dcs;
-        simplify_fn simplifier(tctx, dcs, all_lemmas, max_steps, contextual, lift_eq,
-                               canonize_instances, canonize_proofs, use_axioms);
-        simplifier.set_use_matcher(false); // hack
+        simplify_fn simplifier(tctx, dcs, all_lemmas, cfg);
         auto thm_pr = simplifier.prove_by_simp(get_eq_name(), thm);
         if (!thm_pr) {
             formatter_factory const & fmtf = get_global_ios().get_formatter_factory();
diff --git a/src/library/tactic/simplify.cpp b/src/library/tactic/simplify.cpp
index 4a1e4866a5..f508058499 100644
--- a/src/library/tactic/simplify.cpp
+++ b/src/library/tactic/simplify.cpp
@@ -55,17 +55,31 @@ Author: Daniel Selsam, Leonardo de Moura
 #ifndef LEAN_DEFAULT_SIMPLIFY_LIFT_EQ
 #define LEAN_DEFAULT_SIMPLIFY_LIFT_EQ true
 #endif
-#ifndef LEAN_DEFAULT_SIMPLIFY_DEFEQ_CANONIZE_INSTANCES_FIXED_POINT
-#define LEAN_DEFAULT_SIMPLIFY_DEFEQ_CANONIZE_INSTANCES_FIXED_POINT false
-#endif
-#ifndef LEAN_DEFAULT_SIMPLIFY_DEFEQ_CANONIZE_PROOFS_FIXED_POINT
-#define LEAN_DEFAULT_SIMPLIFY_DEFEQ_CANONIZE_PROOFS_FIXED_POINT false
-#endif
 
 namespace lean {
 #define lean_simp_trace(CTX, N, CODE) lean_trace(N, scope_trace_env _scope1(CTX.env(), CTX); CODE)
 #define lean_simp_trace_d(CTX, N, CODE) lean_trace_d(N, scope_trace_env _scope1(CTX.env(), CTX); CODE)
 
+simplify_config::simplify_config():
+    m_max_steps(LEAN_DEFAULT_SIMPLIFY_MAX_STEPS),
+    m_contextual(LEAN_DEFAULT_SIMPLIFY_CONTEXTUAL),
+    m_lift_eq(LEAN_DEFAULT_SIMPLIFY_LIFT_EQ),
+    m_canonize_instances(true),
+    m_canonize_proofs(false),
+    m_use_axioms(false),
+    m_zeta(false) {
+}
+
+simplify_config::simplify_config(vm_obj const & obj) {
+    m_max_steps          = force_to_unsigned(cfield(obj, 0));
+    m_contextual         = to_bool(cfield(obj, 1));
+    m_lift_eq            = to_bool(cfield(obj, 2));
+    m_canonize_instances = to_bool(cfield(obj, 3));
+    m_canonize_proofs    = to_bool(cfield(obj, 4));
+    m_use_axioms         = to_bool(cfield(obj, 5));
+    m_zeta               = to_bool(cfield(obj, 6));
+}
+
 /* -----------------------------------
    Core simplification procedure.
    ------------------------------------ */
@@ -76,7 +90,7 @@ simp_result simplify_core_fn::join(simp_result const & r1, simp_result const & r
 
 void simplify_core_fn::inc_num_steps() {
     m_num_steps++;
-    if (m_num_steps > m_max_steps)
+    if (m_num_steps > m_cfg.m_max_steps)
         throw exception("simplify failed, maximum number of steps exceeded");
 }
 
@@ -200,7 +214,8 @@ expr simplify_core_fn::defeq_canonize_args_step(expr const & e) {
     for (param_info const & pinfo : info.get_params_info()) {
         lean_assert(i < args.size());
         expr new_a;
-        if ((m_canonize_instances && pinfo.is_inst_implicit()) || (m_canonize_proofs && pinfo.is_prop())) {
+        if ((m_cfg.m_canonize_instances && pinfo.is_inst_implicit()) ||
+            (m_cfg.m_canonize_proofs && pinfo.is_prop())) {
             new_a = m_defeq_canonizer.canonize(args[i], m_need_restart);
             lean_simp_trace(m_ctx, name({"simplify", "canonize"}),
                             tout() << "\n" << args[i] << "\n==>\n" << new_a << "\n";);
@@ -265,11 +280,11 @@ simp_result simplify_core_fn::try_user_congr(expr const & e, simp_lemma const &
         lean_verify(is_simp_relation(tmp_ctx.env(), m_type, h_rel, h_lhs, h_rhs) && is_constant(h_rel));
         {
             relations.push_back(const_name(h_rel));
-            flet<simp_lemmas> set_slss(m_slss, m_contextual ? add_to_slss(m_slss, local_factory.as_buffer()) : m_slss);
+            flet<simp_lemmas> set_slss(m_slss, m_cfg.m_contextual ? add_to_slss(m_slss, local_factory.as_buffer()) : m_slss);
 
             h_lhs = tmp_ctx.instantiate_mvars(h_lhs);
 
-            if (m_contextual || m_rel != const_name(h_rel)) {
+            if (m_cfg.m_contextual || m_rel != const_name(h_rel)) {
                 flet<name> set_name(m_rel, const_name(h_rel));
                 freset<simplify_cache> reset_cache(m_cache);
                 congr_hyp_results.emplace_back(visit(h_lhs, some_expr(e)));
@@ -561,7 +576,7 @@ struct match_fn {
 };
 
 bool simplify_core_fn::match(tmp_type_context & ctx, simp_lemma const & sl, expr const & t) {
-    if (m_use_matcher)
+    if (m_cfg.m_use_matcher)
         return match_fn(ctx, sl.get_id())(sl.get_lhs(), t);
     else
         return ctx.is_def_eq(t, sl.get_lhs());
@@ -743,7 +758,7 @@ simp_result simplify_core_fn::visit(expr const & e, optional<expr> const & paren
         }
     }
 
-    if (m_lift_eq && m_rel != get_eq_name()) {
+    if (m_cfg.m_lift_eq && m_rel != get_eq_name()) {
         simp_result eq_result;
         {
             flet<name> use_eq(m_rel, get_eq_name());
@@ -819,7 +834,10 @@ simp_result simplify_core_fn::visit_pi(expr const & e) {
 }
 
 simp_result simplify_core_fn::visit_let(expr const & e) {
-    return simp_result(e);
+    if (m_cfg.m_zeta)
+        return visit(instantiate(let_body(e), let_value(e)), none_expr());
+    else
+        return simp_result(e);
 }
 
 simp_result simplify_core_fn::visit_macro(expr const & e) {
@@ -835,10 +853,8 @@ optional<pair<simp_result, bool>> simplify_core_fn::post(expr const &, optional<
 }
 
 simplify_core_fn::simplify_core_fn(type_context & ctx, defeq_canonizer::state & dcs, simp_lemmas const & slss,
-                                   unsigned max_steps, bool contextual, bool lift_eq,
-                                   bool canonize_instances, bool canonize_proofs):
-    m_ctx(ctx), m_defeq_canonizer(m_ctx, dcs), m_slss(slss), m_max_steps(max_steps), m_contextual(contextual),
-    m_lift_eq(lift_eq), m_canonize_instances(canonize_instances), m_canonize_proofs(canonize_proofs) {
+                                   simplify_config const & cfg):
+    m_ctx(ctx), m_defeq_canonizer(m_ctx, dcs), m_slss(slss), m_cfg(cfg) {
 }
 
 simp_result simplify_core_fn::simplify(expr const & e) {
@@ -899,15 +915,12 @@ optional<expr> simplify_core_fn::prove_by_simp(name const & rel, expr const & e)
    ------------------------------------ */
 
 simplify_ext_core_fn::simplify_ext_core_fn(type_context & ctx, defeq_can_state & dcs, simp_lemmas const & slss,
-                                           unsigned max_steps, bool contextual, bool lift_eq,
-                                           bool canonize_instances, bool canonize_proofs,
-                                           bool use_axioms):
-    simplify_core_fn(ctx, dcs, slss, max_steps, contextual, lift_eq, canonize_instances, canonize_proofs),
-    m_use_axioms (use_axioms) {
+                                           simplify_config const & cfg):
+    simplify_core_fn(ctx, dcs, slss, cfg) {
 }
 
 simp_result simplify_ext_core_fn::visit_lambda(expr const & e) {
-    if (m_rel != get_eq_name() || !m_use_axioms) return simp_result(e);
+    if (m_rel != get_eq_name() || !m_cfg.m_use_axioms) return simp_result(e);
     type_context::tmp_locals locals(m_ctx);
     expr it = e;
     while (is_lambda(it)) {
@@ -997,7 +1010,7 @@ simp_result simplify_ext_core_fn::imp_congr(expr const & e) {
     expr const & a  = binding_domain(e);
     expr const & b  = binding_body(e);
     simp_result r_a = visit(a, some_expr(e));
-    if (m_contextual) {
+    if (m_cfg.m_contextual) {
         type_context::tmp_locals locals(m_ctx);
         expr h = locals.push_local("_h", r_a.get_new());
         flet<simp_lemmas> set_slss(m_slss, add_to_slss(m_slss, locals.as_buffer()));
@@ -1031,7 +1044,7 @@ simp_result simplify_ext_core_fn::imp_congr(expr const & e) {
 }
 
 simp_result simplify_ext_core_fn::visit_pi(expr const & e) {
-    if ((m_rel == get_eq_name() && m_use_axioms) || m_rel == get_iff_name()) {
+    if ((m_rel == get_eq_name() && m_cfg.m_use_axioms) || m_rel == get_iff_name()) {
         if (m_ctx.is_prop(e)) {
             if (!m_ctx.is_prop(binding_domain(e)))
                 return forall_congr(e);
@@ -1043,9 +1056,9 @@ simp_result simplify_ext_core_fn::visit_pi(expr const & e) {
 }
 
 simp_result simplify_ext_core_fn::visit_let(expr const & e) {
-    /* TODO(Leo): we need to implement efficient code for checking whether the abstraction of
+    /* TODO(Leo): when m_zeta is false, we need to implement efficient code for checking whether the abstraction of
        a let-body is type correct or not */
-    return simp_result(e);
+    return simplify_core_fn::visit_let(e);
 }
 
 static optional<pair<simp_result, bool>> to_ext_result(simp_result const & r) {
@@ -1067,7 +1080,7 @@ optional<pair<simp_result, bool>> simplify_fn::post(expr const & e, optional<exp
     simp_result r = rewrite(e);
     if (r.get_new() != e) {
         return to_ext_result(r);
-    } else if (!m_use_axioms) {
+    } else if (!m_cfg.m_use_axioms) {
         return no_ext_result();
     } else {
         r = propext_rewrite(e);
@@ -1136,13 +1149,9 @@ class vm_simplify_fn : public simplify_ext_core_fn {
     }
 
 public:
-    vm_simplify_fn(type_context & ctx, defeq_can_state & dcs, simp_lemmas const & slss,
-                   unsigned max_steps, bool contextual, bool lift_eq,
-                   bool canonize_instances, bool canonize_proofs, bool use_axioms,
-                   vm_obj const & prove, vm_obj const & pre, vm_obj const & post,
-                   tactic_state const & s):
-        simplify_ext_core_fn(ctx, dcs, slss, max_steps, contextual, lift_eq,
-                             canonize_instances, canonize_proofs, use_axioms),
+    vm_simplify_fn(type_context & ctx, defeq_can_state & dcs, simp_lemmas const & slss, simplify_config const & cfg,
+                   vm_obj const & prove, vm_obj const & pre, vm_obj const & post, tactic_state const & s):
+        simplify_ext_core_fn(ctx, dcs, slss, cfg),
         m_prove(prove), m_pre(pre), m_post(post),
         m_s(s) {}
 
@@ -1153,25 +1162,6 @@ public:
     }
 };
 
-/*
-structure simplify_config :=
-(max_steps : nat)
-(contextual : bool)
-(lift_eq : bool)
-(canonize_instances : bool)
-(canonize_proofs : bool)
-(use_axioms : bool)
-*/
-void get_simplify_config(vm_obj const & obj, unsigned & max_steps, bool & contextual, bool & lift_eq,
-                         bool & canonize_instances, bool & canonize_proofs, bool & use_axioms) {
-    max_steps          = force_to_unsigned(cfield(obj, 0), std::numeric_limits<unsigned>::max());
-    contextual         = to_bool(cfield(obj, 1));
-    lift_eq            = to_bool(cfield(obj, 2));
-    canonize_instances = to_bool(cfield(obj, 3));
-    canonize_proofs    = to_bool(cfield(obj, 4));
-    use_axioms         = to_bool(cfield(obj, 5));
-}
-
 /*
 meta constant simplify_core
   (c : simplify_config)
@@ -1182,12 +1172,10 @@ meta constant simplify_core
 vm_obj tactic_simplify_core(vm_obj const & c, vm_obj const & slss, vm_obj const & rel, vm_obj const & e, vm_obj const & _s) {
     tactic_state const & s   = tactic::to_state(_s);
     try {
-        unsigned max_steps; bool contextual, lift_eq, canonize_instances, canonize_proofs, use_axioms;
-        get_simplify_config(c, max_steps, contextual, lift_eq, canonize_instances, canonize_proofs, use_axioms);
+        simplify_config cfg(c);
         type_context ctx     = mk_type_context_for(s, transparency_mode::Reducible);
         defeq_can_state dcs  = s.dcs();
-        simplify_fn simp(ctx, dcs, to_simp_lemmas(slss), max_steps, contextual, lift_eq,
-                         canonize_instances, canonize_proofs, use_axioms);
+        simplify_fn simp(ctx, dcs, to_simp_lemmas(slss), cfg);
         simp_result result   = simp(to_name(rel), to_expr(e));
         if (result.get_new() != to_expr(e)) {
             result = finalize(ctx, to_name(rel), result);
@@ -1205,12 +1193,10 @@ static vm_obj ext_simplify_core(vm_obj const & a, vm_obj const & c, simp_lemmas
                                 vm_obj const & pre, vm_obj const & post, name const & r, expr const & e,
                                 tactic_state const & s) {
     try {
-        unsigned max_steps; bool contextual, lift_eq, canonize_instances, canonize_proofs, use_axioms;
-        get_simplify_config(c, max_steps, contextual, lift_eq, canonize_instances, canonize_proofs, use_axioms);
+        simplify_config cfg(c);
         type_context ctx     = mk_type_context_for(s, transparency_mode::Reducible);
         defeq_can_state dcs  = s.dcs();
-        vm_simplify_fn simp(ctx, dcs, slss, max_steps, contextual, lift_eq, canonize_instances, canonize_proofs,
-                            use_axioms, prove, pre, post, s);
+        vm_simplify_fn simp(ctx, dcs, slss, cfg, prove, pre, post, s);
         pair<vm_obj, simp_result> p = simp(a, r, e);
         if (p.second.get_new() != e) {
             vm_obj const & a   = p.first;
diff --git a/src/library/tactic/simplify.h b/src/library/tactic/simplify.h
index 7e8fc0bfd1..f5a2ab618a 100644
--- a/src/library/tactic/simplify.h
+++ b/src/library/tactic/simplify.h
@@ -12,6 +12,32 @@ Author: Daniel Selsam, Leonardo de Moura
 #include "library/tactic/simp_result.h"
 
 namespace lean {
+
+/*
+structure simplify_config :=
+(max_steps : nat)
+(contextual : bool)
+(lift_eq : bool)
+(canonize_instances : bool)
+(canonize_proofs : bool)
+(use_axioms : bool)
+(zeta : bool)
+*/
+struct simplify_config {
+    unsigned                  m_max_steps;
+    bool                      m_contextual;
+    bool                      m_lift_eq;
+    bool                      m_canonize_instances;
+    bool                      m_canonize_proofs;
+    bool                      m_use_axioms;
+    bool                      m_zeta;
+    /* The following option should be removed as soon as we
+       refactor the inductive compiler. */
+    bool                      m_use_matcher{true};
+    simplify_config();
+    simplify_config(vm_obj const & o);
+};
+
 /* Core simplification procedure. It performs the following tasks:
    1- Manages the cache;
    2- Applies congruence lemmas;
@@ -46,19 +72,14 @@ protected:
     bool                      m_need_restart{false};
 
     /* Options */
-    unsigned                  m_max_steps;
-    bool                      m_contextual;
-    bool                      m_lift_eq;
-    bool                      m_canonize_instances;
-    bool                      m_canonize_proofs;
-    /* The following option should be removed as soon as we
-       refactor the inductive compiler. */
-    bool                      m_use_matcher{true};
+    simplify_config           m_cfg;
 
     simp_result join(simp_result const & r1, simp_result const & r2);
     void inc_num_steps();
     bool is_dependent_fn(expr const & f);
-    bool should_defeq_canonize() const { return m_canonize_instances || m_canonize_proofs; }
+    bool should_defeq_canonize() const {
+        return m_cfg.m_canonize_instances || m_cfg.m_canonize_proofs;
+    }
     bool instantiate_emetas(tmp_type_context & tmp_tctx, unsigned num_emeta,
                             list<expr> const & emetas, list<bool> const & instances);
     simp_result lift_from_eq(simp_result const & r_eq);
@@ -107,14 +128,11 @@ protected:
 
 public:
     simplify_core_fn(type_context & ctx, defeq_canonizer::state & dcs, simp_lemmas const & slss,
-                     unsigned max_steps, bool contextual, bool lift_eq,
-                     bool canonize_instances, bool canonize_proofs);
+                     simplify_config const & cfg);
 
     environment const & env() const;
     simp_result operator()(name const & rel, expr const & e);
 
-    void set_use_matcher(bool flag) { m_use_matcher = flag; }
-
     optional<expr> prove_by_simp(name const & rel, expr const & e);
 };
 
@@ -122,7 +140,6 @@ public:
    extensionality and propositional extensionality. */
 class simplify_ext_core_fn : public simplify_core_fn {
 protected:
-    bool m_use_axioms;
     simp_result forall_congr(expr const & e);
     simp_result imp_congr(expr const & e);
     virtual simp_result visit_lambda(expr const & e) override;
@@ -130,8 +147,7 @@ protected:
     virtual simp_result visit_let(expr const & e) override;
 public:
     simplify_ext_core_fn(type_context & ctx, defeq_canonizer::state & dcs, simp_lemmas const & slss,
-                         unsigned max_steps, bool contextual, bool lift_eq,
-                         bool canonize_instances, bool canonize_proofs, bool use_axioms);
+                         simplify_config const & cfg);
 };
 
 /* Default (bottom-up) simplifier: reduce projections, apply simplification lemmas,
@@ -143,10 +159,8 @@ protected:
     virtual optional<expr> prove(expr const & e) override;
 public:
     simplify_fn(type_context & ctx, defeq_canonizer::state & dcs, simp_lemmas const & slss,
-                unsigned max_steps, bool contextual, bool lift_eq,
-                bool canonize_instances, bool canonize_proofs, bool use_axioms):
-        simplify_ext_core_fn(ctx, dcs, slss, max_steps, contextual, lift_eq,
-                             canonize_instances, canonize_proofs, use_axioms) {}
+                simplify_config const & cfg):
+        simplify_ext_core_fn(ctx, dcs, slss, cfg) {}
 };
 
 void initialize_simplify();
diff --git a/src/library/tactic/smt/smt_state.cpp b/src/library/tactic/smt/smt_state.cpp
index daca73ffc0..812b81a51e 100644
--- a/src/library/tactic/smt/smt_state.cpp
+++ b/src/library/tactic/smt/smt_state.cpp
@@ -209,15 +209,15 @@ static dsimplify_fn mk_dsimp(type_context & ctx, defeq_can_state & dcs, smt_pre_
 }
 
 static simplify_fn mk_simp(type_context & ctx, defeq_can_state & dcs, smt_pre_config const & cfg) {
-    unsigned max_steps       = cfg.m_max_steps;
-    bool contextual          = false;
-    bool lift_eq             = true;
-    bool canonize_instances  = true;
-    bool canonize_proofs     = false;
-    bool use_axioms          = true;
-    return simplify_fn(ctx, dcs, cfg.m_simp_lemmas, max_steps,
-                       contextual, lift_eq, canonize_instances,
-                       canonize_proofs, use_axioms);
+    simplify_config scfg;
+    scfg.m_max_steps          = cfg.m_max_steps;
+    scfg.m_contextual         = false;
+    scfg.m_lift_eq            = true;
+    scfg.m_canonize_instances = true;
+    scfg.m_canonize_proofs    = false;
+    scfg.m_use_axioms         = true;
+    scfg.m_zeta               = cfg.m_zeta;
+    return simplify_fn(ctx, dcs, cfg.m_simp_lemmas, scfg);
 }
 
 static simp_result preprocess(type_context & ctx, defeq_can_state & dcs, smt_pre_config const & cfg, expr const & e) {
diff --git a/tests/lean/run/1315b.lean b/tests/lean/run/1315b.lean
index 8225f0b972..52f8988eb3 100644
--- a/tests/lean/run/1315b.lean
+++ b/tests/lean/run/1315b.lean
@@ -63,6 +63,6 @@ begin
   induction n with n',
   {intro, reflexivity},
   {intro,
-   simp [test], dsimp, simp [ih_1],
+   simp [test] {zeta := ff}, dsimp, simp [ih_1],
    simp [nat.bit1_eq_succ_bit0, test]}
 end
diff --git a/tests/lean/run/auto_propext.lean b/tests/lean/run/auto_propext.lean
index 22ab32acfd..168cc82d4b 100644
--- a/tests/lean/run/auto_propext.lean
+++ b/tests/lean/run/auto_propext.lean
@@ -2,4 +2,4 @@ example (p q : Prop) (h : p) : q ∨ p :=
 by simp [h]
 
 example (p q : Prop) : p → q ∨ p :=
-by ctx_simp
+by simp {contextual := tt}
diff --git a/tests/lean/run/interactive1.lean b/tests/lean/run/interactive1.lean
index ddb2a621db..3fa121f57a 100644
--- a/tests/lean/run/interactive1.lean
+++ b/tests/lean/run/interactive1.lean
@@ -45,4 +45,4 @@ begin
 end
 open tactic
 example (a b : nat) : a = b → h 0 a = b :=
-by ctx_simp without bla
+by simp without bla {contextual := tt}
diff --git a/tests/lean/run/rw_set4.lean b/tests/lean/run/rw_set4.lean
index 479d268170..52a4f66040 100644
--- a/tests/lean/run/rw_set4.lean
+++ b/tests/lean/run/rw_set4.lean
@@ -7,5 +7,5 @@ sorry
 
 print [congr] default
 
-example (A : Type) (a b c : A) : (a = b) → (a = c) → a = b := by ctx_simp
-example (A : Type) (a b c : A) : (a = c) → (a = b) → a = b := by ctx_simp
+example (A : Type) (a b c : A) : (a = b) → (a = c) → a = b := by simp {contextual := tt}
+example (A : Type) (a b c : A) : (a = c) → (a = b) → a = b := by simp {contextual := tt}
diff --git a/tmp/mini_crush.lean b/tmp/mini_crush.lean
index 5878014628..da39bce99e 100644
--- a/tmp/mini_crush.lean
+++ b/tmp/mini_crush.lean
@@ -3,6 +3,7 @@ declare_trace mini_crush
 namespace mini_crush
 open smt_tactic tactic
 
+/- Collect relevant functions -/
 meta def is_auto_construction : name → bool
 | (name.mk_string "brec_on" p)      := tt
 | (name.mk_string "cases_on" p)     := tt
@@ -36,6 +37,24 @@ do ctx ← local_context,
    s₁  ← mfoldl (λ s e, infer_type e >>= collect_revelant_fns_aux s) mk_name_set ctx,
    target >>= collect_revelant_fns_aux s₁
 
+/- repeat simp & intro -/
+
+meta def simph_and_intro_aux : simp_lemmas → tactic unit
+| S := do
+  t ← target,
+
+
+return ()
+
+meta def simph_and_intro : tactic unit :=
+do S ← simp_lemmas.mk_default,
+   S ← collect_ctx_simps >>= S^.append,
+   simph_and_intro_aux S
+
+
+meta def collect_ctx_simps : tactic (list expr) :=
+
+
 meta def size (e : expr) : nat :=
 e^.fold 1 (λ e _ n, n+1)