diff --git a/library/standard/tactic.lean b/library/standard/tactic.lean
index 4863eeb27..ca0a26232 100644
--- a/library/standard/tactic.lean
+++ b/library/standard/tactic.lean
@@ -31,4 +31,5 @@ definition trace      (s : string) : tactic := tactic_value
 infixl `;`:200         := and_then
 infixl `|`:100         := or_else
 notation `!`:max t:max := repeat t
+notation `⟦` t `⟧`     := apply t
 end
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index c58b3b1f3..07f7768db 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -663,12 +663,12 @@ public:
                 mvar = update_mlocal(mvar, subst.instantiate_metavars_wo_jst(mlocal_type(mvar)));
                 meta = ::lean::mk_app(mvar, locals);
                 expr type = m_tc.infer(*meta);
-                proof_state ps = to_proof_state(*meta, type, m_ngen.mk_child());
+                proof_state ps(goals(goal(*meta, type)), subst, m_ngen.mk_child());
                 if (optional<tactic> t = get_tactic_for(subst, mvar)) {
                     proof_state_seq seq = (*t)(m_env, m_ios, ps);
                     if (auto r = seq.pull()) {
-                        substitution s = r->first.get_subst();
-                        expr v = s.instantiate_metavars_wo_jst(mvar);
+                        subst = r->first.get_subst();
+                        expr v = subst.instantiate_metavars_wo_jst(mvar);
                         if (has_metavar(v)) {
                             display_unsolved_proof_state(mvar, r->first, "unsolved subgoals");
                         } else {
diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp
index 442122569..690b1def6 100644
--- a/src/library/tactic/apply_tactic.cpp
+++ b/src/library/tactic/apply_tactic.cpp
@@ -37,84 +37,66 @@ bool collect_simple_metas(expr const & e, buffer<expr> & result) {
     return !failed;
 }
 
-tactic apply_tactic(expr const & e) {
-    return tactic([=](environment const &, io_state const &, proof_state const & s) {
-            std::cout << e << "\n";
-            return s;
-#if 0
-            if (s.is_final_state()) {
-                return proof_state_seq();
+unsigned get_expect_num_args(type_checker & tc, expr e) {
+    unsigned r = 0;
+    while (true) {
+        e = tc.whnf(e);
+        if (!is_pi(e))
+            return r;
+        e = binding_body(e);
+        r++;
+    }
+}
+
+void collect_simple_meta(expr const & e, buffer<expr> & metas) {
+    for_each(e, [&](expr const & e, unsigned) {
+            if (is_meta(e)) {
+                if (is_simple_meta(e))
+                    metas.push_back(e);
+                return false; /* do not visit its type */
             }
-            goals const & gs    = s.get_goals();
-            name gname          = head(gs).first;
-            goal  g             = head(gs).second;
-            goals rest_gs       = tail(gs);
-            expr const & C      = g.get_conclusion();
-            name_generator ngen = s.ngen();
+            return has_metavar(e);
+        });
+}
+
+tactic apply_tactic(expr const & _e) {
+    return tactic([=](environment const & env, io_state const & ios, proof_state const & s) {
+            goals const & gs = s.get_goals();
+            if (empty(gs))
+                return proof_state_seq();
+            name_generator ngen = s.get_ngen();
             type_checker tc(env, ngen.mk_child());
-            expr new_e          = e;
-            expr new_e_type     = tc.infer(new_e);
-            buffer<expr> meta_buffer;
-            if (!collect_simple_metas(new_e, meta_buffer))
-                return proof_state_seq();
-            // add more metavariables while new_e_type is a Pi
-            while (is_pi(new_e_type)) {
-                expr meta  = g.mk_meta(ngen.next(), binding_domain(new_e_type));
-                meta_buffer.push_back(meta);
-                new_e      = mk_app(new_e, meta);
-                new_e_type = instantiate(binding_body(new_e_type), meta);
+            goal  g          = head(gs);
+            goals tail_gs    = tail(gs);
+            expr  t          = g.get_type();
+            expr  e          = _e;
+            expr  e_t        = tc.infer(e);
+            unsigned num_t   = get_expect_num_args(tc, t);
+            unsigned num_e_t = get_expect_num_args(tc, e_t);
+            if (num_t > num_e_t)
+                return proof_state_seq(); // no hope to unify then
+            for (unsigned i = 0; i < num_e_t - num_t; i++) {
+                e_t        = tc.whnf(e_t);
+                expr meta  = g.mk_meta(ngen.next(), binding_domain(e_t));
+                e          = mk_app(e, meta);
+                e_t        = instantiate(binding_body(e_t), meta);
             }
-            list<expr> metas = to_list(meta_buffer.begin(), meta_buffer.end());
-            // TODO(Leo): we should use unifier plugin
-            lazy_list<substitution> substs = unify(env, C, new_e_type, ngen.mk_child(), ios.get_options());
+            lazy_list<substitution> substs = unify(env, t, e_t, ngen.mk_child(), s.get_subst(), ios.get_options());
             return map2<proof_state>(substs, [=](substitution const & subst) -> proof_state {
-                    // apply substitution to remaining goals
                     name_generator new_ngen(ngen);
                     type_checker tc(env, new_ngen.mk_child());
-                    goals new_gs = map(rest_gs, [&](named_goal const & ng) {
-                            return named_goal(ng.first, ng.second.instantiate_metavars(subst));
-                        });
-                    expr P            = subst.instantiate_metavars_wo_jst(new_e);
-                    goal tmp_g        = g.instantiate_metavars(subst);
-                    unsigned subgoal_idx = 1;
-                    buffer<std::pair<name, expr>> trace_buffer;
-                    // add unassigned metavariables as new goals
-                    buffer<named_goal> subgoals;
-                    for (expr const & meta : metas) {
-                        if (!subst.is_assigned(get_app_fn(meta))) {
-                            name new_gname(gname, subgoal_idx);
-                            expr new_C = subst.instantiate_metavars_wo_jst(tc.infer(meta));
-                            goal new_g(tmp_g.get_hypotheses(), new_C);
-                            subgoals.emplace_back(new_gname, new_g);
-                            trace_buffer.emplace_back(new_gname, meta);
-                            subgoal_idx++;
-                        }
+                    expr new_e = subst.instantiate_metavars_wo_jst(e);
+                    substitution new_subst = subst.assign(g.get_name(), g.abstract(new_e));
+                    buffer<expr> metas;
+                    collect_simple_meta(new_e, metas);
+                    goals new_gs = tail_gs;
+                    unsigned i = metas.size();
+                    while (i > 0) {
+                        --i;
+                        new_gs = cons(goal(metas[i], subst.instantiate_metavars_wo_jst(tc.infer(metas[i]))), new_gs);
                     }
-                    new_gs = to_list(subgoals.begin(), subgoals.end(), new_gs);
-                    list<std::pair<name, expr>> trace = to_list(trace_buffer.begin(), trace_buffer.end());
-                    proof_builder pb = s.get_pb();
-                    proof_builder new_pb([=](proof_map const & m, substitution const & pb_subst) {
-                            proof_map new_m(m);
-                            substitution new_subst;
-                            for (auto const & p : trace) {
-                                expr pr   = find(new_m, p.first);
-                                expr meta = p.second;
-                                buffer<expr> meta_args;
-                                expr mvar = get_app_args(meta, meta_args);
-                                unsigned i = meta_args.size();
-                                while (i > 0) {
-                                    --i;
-                                    pr = Fun(meta_args[i], pr);
-                                }
-                                new_subst = new_subst.assign(mlocal_name(mvar), pr, justification());
-                                new_m.erase(p.first);
-                            }
-                            new_m.insert(gname, new_subst.instantiate_metavars_wo_jst(P));
-                            return pb(new_m, pb_subst);
-                        });
-                    return proof_state(s, new_gs, new_pb, new_ngen);
+                    return proof_state(new_gs, new_subst, new_ngen);
                 });
-#endif
         });
 }
 
diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp
index eb589b61a..40c7560ee 100644
--- a/src/library/tactic/tactic.cpp
+++ b/src/library/tactic/tactic.cpp
@@ -175,6 +175,7 @@ tactic take(tactic const & t, unsigned k) {
 tactic assumption_tactic() {
     return tactic01([](environment const &, io_state const &, proof_state const & s) -> optional<proof_state> {
             substitution subst = s.get_subst();
+            bool solved = false;
             goals new_gs = map_goals(s, [&](goal const & g) -> optional<goal> {
                     expr const & t  = g.get_type();
                     optional<expr> h;
@@ -187,13 +188,17 @@ tactic assumption_tactic() {
                         }
                     }
                     if (h) {
-                        subst = subst.assign(g.get_mvar(), g.abstract(*h), justification());
+                        subst  = subst.assign(g.get_mvar(), g.abstract(*h), justification());
+                        solved = true;
                         return optional<goal>();
                     } else {
                         return some(g);
                     }
                 });
-            return some(proof_state(s, new_gs, subst));
+            if (solved)
+                return some(proof_state(s, new_gs, subst));
+            else
+                return none_proof_state();
         });
 }
 
diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp
index dd54a6d17..87614133f 100644
--- a/src/library/unifier.cpp
+++ b/src/library/unifier.cpp
@@ -1186,8 +1186,7 @@ lazy_list<substitution> unify(environment const & env, unsigned num_cs, constrai
 }
 
 lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, unifier_plugin const & p,
-                              unsigned max_steps) {
-    substitution s;
+                              substitution const & s, unsigned max_steps) {
     name_generator new_ngen(ngen);
     type_checker tc(env, new_ngen.mk_child());
     if (!tc.is_def_eq(lhs, rhs))
@@ -1204,16 +1203,18 @@ lazy_list<substitution> unify(environment const & env, expr const & lhs, expr co
 }
 
 lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, unifier_plugin const & p,
-                              options const & o) {
-    return unify(env, lhs, rhs, ngen, p, get_unifier_max_steps(o));
+                              substitution const & s, options const & o) {
+    return unify(env, lhs, rhs, ngen, p, s, get_unifier_max_steps(o));
 }
 
-lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, unsigned max_steps) {
-    return unify(env, lhs, rhs, ngen, [](constraint const &, name_generator const &) { return lazy_list<constraints>(); }, max_steps);
+lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen,
+                              substitution const & s, unsigned max_steps) {
+    return unify(env, lhs, rhs, ngen, [](constraint const &, name_generator const &) { return lazy_list<constraints>(); }, s, max_steps);
 }
 
-lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, options const & o) {
-    return unify(env, lhs, rhs, ngen, get_unifier_max_steps(o));
+lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen,
+                              substitution const & s, options const & o) {
+    return unify(env, lhs, rhs, ngen, s, get_unifier_max_steps(o));
 }
 
 static int unify_simple(lua_State * L) {
@@ -1335,39 +1336,15 @@ static int unify(lua_State * L) {
     lazy_list<substitution> r;
     environment const & env = to_environment(L, 1);
     if (is_expr(L, 2)) {
-        if (nargs == 3)
-            r = unify(env, to_expr(L, 2), to_expr(L, 3), name_generator(g_tmp_prefix));
-        else if (nargs == 4 && is_options(L, 4))
-            r = unify(env, to_expr(L, 2), to_expr(L, 3), name_generator(g_tmp_prefix), to_options(L, 4));
-        else if (nargs == 4 && is_name_generator(L, 4))
-            r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4));
-        else if (nargs == 4)
-            r = unify(env, to_expr(L, 2), to_expr(L, 3), name_generator(g_tmp_prefix), to_unifier_plugin(L, 4));
-        else if (nargs == 5 && is_name_generator(L, 4) && is_options(L, 5))
-            r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), to_options(L, 5));
-        else if (nargs == 5 && is_options(L, 5))
-            r = unify(env, to_expr(L, 2), to_expr(L, 3), name_generator(g_tmp_prefix), to_unifier_plugin(L, 4), to_options(L, 5));
-        else if (nargs == 5)
-            r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), to_unifier_plugin(L, 5));
+        if (nargs == 6 && is_substitution(L, 5))
+            r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), to_substitution(L, 5), to_options(L, 6));
         else
-            r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), to_unifier_plugin(L, 5), to_options(L, 6));
+            r = unify(env, to_expr(L, 2), to_expr(L, 3), to_name_generator(L, 4), to_unifier_plugin(L, 5), to_substitution(L, 6), to_options(L, 7));
     } else {
         buffer<constraint> cs;
         to_constraint_buffer(L, 2, cs);
-        if (nargs == 2)
-            r = unify(env, cs.size(), cs.data(), name_generator(g_tmp_prefix));
-        else if (nargs == 3 && is_name_generator(L, 3))
-            r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3));
-        else if (nargs == 3 && is_options(L, 3))
-            r = unify(env, cs.size(), cs.data(), name_generator(g_tmp_prefix), to_options(L, 3));
-        else if (nargs == 3)
-            r = unify(env, cs.size(), cs.data(), name_generator(g_tmp_prefix), to_unifier_plugin(L, 3));
-        else if (nargs == 4 && is_name_generator(L, 3) && is_options(L, 4))
+        if (nargs == 4 && is_options(L, 4))
             r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3), to_options(L, 4));
-        else if (nargs == 4 && is_options(L, 4))
-            r = unify(env, cs.size(), cs.data(), name_generator(g_tmp_prefix), to_unifier_plugin(L, 3), to_options(L, 4));
-        else if (nargs == 4)
-            r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3), to_unifier_plugin(L, 4));
         else
             r = unify(env, cs.size(), cs.data(), to_name_generator(L, 3), to_unifier_plugin(L, 4), to_options(L, 5));
     }
diff --git a/src/library/unifier.h b/src/library/unifier.h
index 9ea4fe359..9d933041d 100644
--- a/src/library/unifier.h
+++ b/src/library/unifier.h
@@ -52,13 +52,13 @@ lazy_list<substitution> unify(environment const & env, unsigned num_cs, constrai
 lazy_list<substitution> unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen,
                               options const & o);
 lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, unifier_plugin const & p,
-                              unsigned max_steps = LEAN_DEFAULT_UNIFIER_MAX_STEPS);
+                              substitution const & s = substitution(), unsigned max_steps = LEAN_DEFAULT_UNIFIER_MAX_STEPS);
 lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen,
-                              unsigned max_sharing = LEAN_DEFAULT_UNIFIER_MAX_STEPS);
+                              substitution const & s = substitution(), unsigned max_steps = LEAN_DEFAULT_UNIFIER_MAX_STEPS);
 lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, unifier_plugin const & p,
-                              options const & o);
+                              substitution const & s, options const & o);
 lazy_list<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen,
-                              options const & o);
+                              substitution const & s, options const & o);
 
 class unifier_exception : public exception {
     justification m_jst;
diff --git a/tests/lean/run/tactic10.lean b/tests/lean/run/tactic10.lean
index b81dacb67..b2f9cb3e3 100644
--- a/tests/lean/run/tactic10.lean
+++ b/tests/lean/run/tactic10.lean
@@ -1,7 +1,9 @@
-import logic
+import standard
+using tactic
 
-exit -- TODO
 theorem tst (a b : Bool) (H : a ↔ b) : b ↔ a
-:= by (apply iff_intro,
-       assume Hb, iff_mp_right H Hb,
-       assume Ha, iff_mp_left H Ha)
+:= by apply iff_intro;
+      ⟦ assume Hb, iff_mp_right H Hb ⟧;
+      ⟦ assume Ha, iff_mp_left H Ha ⟧
+
+check tst
diff --git a/tests/lean/run/tactic7.lean b/tests/lean/run/tactic7.lean
index 8268ceb6e..fb2146474 100644
--- a/tests/lean/run/tactic7.lean
+++ b/tests/lean/run/tactic7.lean
@@ -1,5 +1,12 @@
-import logic
+import standard
+using tactic
 
-exit -- TODO
 theorem tst {A B : Bool} (H1 : A) (H2 : B) : A ∧ B ∧ A
-:= by (print, apply and_intro, print, exact, apply and_intro, print, !exact)
+:= by apply and_intro; state; exact; apply and_intro; !exact
+check tst
+
+theorem tst2 {A B : Bool} (H1 : A) (H2 : B) : A ∧ B ∧ A
+:= by !((apply @and_intro | exact) ; trace "STEP"; state; trace "----------")
+
+check tst2
+
diff --git a/tests/lean/run/tactic8.lean b/tests/lean/run/tactic8.lean
index 906de3d96..aae365ab2 100644
--- a/tests/lean/run/tactic8.lean
+++ b/tests/lean/run/tactic8.lean
@@ -1,8 +1,9 @@
-import logic
+import standard
+using tactic
 
-exit -- TODO
 theorem tst {A B : Bool} (H1 : A) (H2 : B) : A ∧ B ∧ A
-:= by (apply and_intro,
-       show A, from H1,
-       show B ∧ A, from and_intro H2 H1)
+:= by (apply @and_intro;
+       apply (show A, from H1);
+       apply (show B ∧ A, from and_intro H2 H1))
+
 check @tst
\ No newline at end of file
diff --git a/tests/lean/run/tactic9.lean b/tests/lean/run/tactic9.lean
index 49dba3a6b..4d2969139 100644
--- a/tests/lean/run/tactic9.lean
+++ b/tests/lean/run/tactic9.lean
@@ -1,5 +1,6 @@
-import logic
+import standard
+using tactic
 
-exit -- TODO
 theorem tst {A B : Bool} (H1 : A) (H2 : B) : ((fun x : Bool, x) A) ∧ B ∧ A
-:= by (apply and_intro, beta, exact, apply and_intro, !exact)
+:= by apply and_intro; beta; exact; apply and_intro; !exact
+
diff --git a/tests/lua/unify2.lua b/tests/lua/unify2.lua
index 5f95c97cf..f1cf56e9b 100644
--- a/tests/lua/unify2.lua
+++ b/tests/lua/unify2.lua
@@ -1,6 +1,6 @@
 function test_unify(env, lhs, rhs, num_s)
    print(tostring(lhs) .. " =?= " .. tostring(rhs) .. ", expected: " .. tostring(num_s))
-   local ss = unify(env, lhs, rhs)
+   local ss = unify(env, lhs, rhs, name_generator(), substitution(), options())
    local n  = 0
    for s in ss do
       print("solution: ")
diff --git a/tests/lua/unify3.lua b/tests/lua/unify3.lua
index 4e4bfdf84..572bc7068 100644
--- a/tests/lua/unify3.lua
+++ b/tests/lua/unify3.lua
@@ -15,7 +15,7 @@ local m = mk_metavar("m", mk_metavar("m_ty", mk_sort(mk_meta_univ("u"))))
 local cs  = { mk_eq_cnstr(carrier(m), real) }
 local o   = options({"unifier", "use_exceptions"}, false)
 print(o)
-assert(not unify(env, cs, o)())
+assert(not unify(env, cs, name_generator(), o)())
 
 function hint(c, ngen)
    local lhs = c:lhs()
@@ -44,4 +44,4 @@ function display_solutions(ss)
    end
 end
 
-display_solutions(unify(env, cs, hint, o))
+display_solutions(unify(env, cs, name_generator(), hint, o))
diff --git a/tests/lua/unify4.lua b/tests/lua/unify4.lua
index 2d68d4654..8b6f6032a 100644
--- a/tests/lua/unify4.lua
+++ b/tests/lua/unify4.lua
@@ -1,6 +1,6 @@
 function test_unify(env, m, lhs, rhs, num_s)
    print(tostring(lhs) .. " =?= " .. tostring(rhs) .. ", expected: " .. tostring(num_s))
-   local ss = unify(env, lhs, rhs)
+   local ss = unify(env, lhs, rhs, name_generator(), substitution(), options())
    local n  = 0
    for s in ss do
       print("solution: " .. tostring(s:instantiate(m)))
diff --git a/tests/lua/unify5.lua b/tests/lua/unify5.lua
index 5e96f23da..ed8c1c7b2 100644
--- a/tests/lua/unify5.lua
+++ b/tests/lua/unify5.lua
@@ -34,4 +34,4 @@ cs = { mk_eq_cnstr(m1, f(m2, f(m3, m4))),
        mk_choice_cnstr(m4, function(e, s, ngen) return {a, b} end)
      }
 
-display_solutions(m1, unify(env, cs, o))
+display_solutions(m1, unify(env, cs, name_generator(), o))
diff --git a/tests/lua/unify6.lua b/tests/lua/unify6.lua
index 6a49bccda..f65c577e1 100644
--- a/tests/lua/unify6.lua
+++ b/tests/lua/unify6.lua
@@ -24,4 +24,4 @@ cs = { mk_level_eq_cnstr(m1, max_univ(m2, max_univ(m2, l1, 1))),
        mk_level_eq_cnstr(m3+1, m2+1)
      }
 
-display_solutions(m1, unify(env, cs, o))
+display_solutions(m1, unify(env, cs, name_generator(), o))
diff --git a/tests/lua/unify7.lua b/tests/lua/unify7.lua
index f45352142..9f6aae62d 100644
--- a/tests/lua/unify7.lua
+++ b/tests/lua/unify7.lua
@@ -11,7 +11,7 @@ local m   = mk_metavar("m", mk_arrow(N, N, Type))
 local cs  = { mk_eq_cnstr(m(a, a), t) }
 
 local o   = options({"unifier", "use_exceptions"}, false)
-ss = unify(env, cs, o)
+ss = unify(env, cs, name_generator(), o)
 local n = 0
 for s in ss do
    print("solution: " .. tostring(s:instantiate(m)))