diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp
index 638351ac4..a9fe63399 100644
--- a/src/library/tactic/apply_tactic.cpp
+++ b/src/library/tactic/apply_tactic.cpp
@@ -70,11 +70,12 @@ static proof_state_seq apply_tactic_core(environment const & env, io_state const
     expr  e_t        = e_t_cs.first;
     buffer<expr> metas;
     if (add_meta) {
-        unsigned num_t   = get_expect_num_args(*tc, t);
+        // 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++) {
+        // Remark: we used to add (num_e_t - num_t) arguments.
+        // This would allow us to handle (A -> B) without using intros,
+        // but it was preventing us from solving other problems
+        for (unsigned i = 0; i < num_e_t; i++) {
             auto e_t_cs = tc->whnf(e_t);
             e_t_cs.second.linearize(cs);
             e_t        = e_t_cs.first;
diff --git a/tests/lean/run/tactic10.lean b/tests/lean/run/tactic10.lean
index b97715092..fa0daaf29 100644
--- a/tests/lean/run/tactic10.lean
+++ b/tests/lean/run/tactic10.lean
@@ -2,7 +2,9 @@ import logic
 
 theorem tst (a b : Prop) (H : a ↔ b) : b ↔ a
 := by rapply iff.intro;
-      apply (assume Ha, iff.elim_left H Ha);
-      apply (assume Hb, iff.elim_right H Hb)
+      intro Ha;
+        apply (iff.elim_left H Ha);
+      intro Hb;
+        apply (iff.elim_right H Hb)
 
 check tst
diff --git a/tests/lean/run/tactic11.lean b/tests/lean/run/tactic11.lean
index 400bc2035..32e9e1bed 100644
--- a/tests/lean/run/tactic11.lean
+++ b/tests/lean/run/tactic11.lean
@@ -4,14 +4,18 @@ theorem tst (a b : Prop) (H : a ↔ b) : b ↔ a
 := have H1 [visible] : a → b, -- We need to mark H1 as fact, otherwise it is not visible by tactics
    from iff.elim_left H,
    by rapply iff.intro;
-      apply (assume Ha, H1 Ha);
-      apply (assume Hb, iff.elim_right H Hb)
+      intro Ha;
+        apply (H1 Ha);
+      intro Hb;
+        apply (iff.elim_right H Hb)
 
 theorem tst2 (a b : Prop) (H : a ↔ b) : b ↔ a
 := have H1 [visible] : a → b,
    from iff.elim_left H,
    begin
      rapply iff.intro,
-     apply (assume Ha, H1 Ha),
-     apply (assume Hb, iff.elim_right H Hb)
+     intro Ha;
+       apply (H1 Ha),
+     intro Hb;
+       apply (iff.elim_right H Hb)
    end
diff --git a/tests/lean/run/tactic12.lean b/tests/lean/run/tactic12.lean
index c09288c2c..8a1a5d7eb 100644
--- a/tests/lean/run/tactic12.lean
+++ b/tests/lean/run/tactic12.lean
@@ -4,7 +4,6 @@ open tactic
 theorem tst (a b : Prop) (H : ¬ a ∨ ¬ b) (Hb : b) : ¬ a ∧ b
 := by apply and.intro;
       assumption;
-      apply not_intro;
       exact
         (assume Ha, or.elim H
           (assume Hna, @absurd _ false Ha Hna)
diff --git a/tests/lean/run/tactic13.lean b/tests/lean/run/tactic13.lean
index c51161b9f..bf28801f7 100644
--- a/tests/lean/run/tactic13.lean
+++ b/tests/lean/run/tactic13.lean
@@ -5,7 +5,6 @@ theorem tst (a b : Prop) (H : ¬ a ∨ ¬ b) (Hb : b) : ¬ a ∧ b :=
 begin
   apply and.intro,
   assumption,
-  apply not_intro,
   assume Ha, or.elim H
     (assume Hna, @absurd _ false Ha Hna)
     (assume Hnb, @absurd _ false Hb Hnb)