diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp
index fd28da4bdb..478d820901 100644
--- a/src/library/tactic/tactic.cpp
+++ b/src/library/tactic/tactic.cpp
@@ -132,35 +132,7 @@ tactic try_for(tactic t, unsigned ms, unsigned check_ms) {
         check_ms = 1;
     return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq {
             tactic _t(t);
-            proof_state_seq         r;
-            std::atomic<bool>       done(false);
-            interruptible_thread th([&]() {
-                    try {
-                        r = _t(env, io, s);
-                    } catch (...) {
-                        r = proof_state_seq();
-                    }
-                    done = true;
-                });
-            try {
-                auto start = std::chrono::steady_clock::now();
-                std::chrono::milliseconds d(ms);
-                std::chrono::milliseconds small(check_ms);
-                while (!done) {
-                    auto curr = std::chrono::steady_clock::now();
-                    if (std::chrono::duration_cast<std::chrono::milliseconds>(curr - start) > d)
-                        break;
-                    check_interrupted();
-                    std::this_thread::sleep_for(small);
-                }
-                th.request_interrupt();
-                th.join();
-                return r;
-            } catch (...) {
-                th.request_interrupt();
-                th.join();
-                throw;
-            }
+            return timeout(_t(env, io, s), ms, check_ms);
         });
 }
 
@@ -184,44 +156,7 @@ tactic par(tactic t1, tactic t2, unsigned check_ms) {
     return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq {
             tactic _t1(t1);
             tactic _t2(t2);
-            proof_state_seq r1;
-            proof_state_seq r2;
-            std::atomic<bool>  done1(false);
-            std::atomic<bool>  done2(false);
-            interruptible_thread th1([&]() {
-                    try {
-                        r1 = _t1(env, io, s);
-                    } catch (...) {
-                        r1 = proof_state_seq();
-                    }
-                    done1 = true;
-                });
-            interruptible_thread th2([&]() {
-                    try {
-                        r2 = _t2(env, io, s);
-                    } catch (...) {
-                        r2 = proof_state_seq();
-                    }
-                    done2 = true;
-                });
-            try {
-                std::chrono::milliseconds small(check_ms);
-                while (!done1 && !done2) {
-                    check_interrupted();
-                    std::this_thread::sleep_for(small);
-                }
-                th1.request_interrupt();
-                th2.request_interrupt();
-                th1.join();
-                th2.join();
-                return orelse(r1, r2);
-            } catch (...) {
-                th1.request_interrupt();
-                th2.request_interrupt();
-                th1.join();
-                th2.join();
-                throw;
-            }
+            return par(_t1(env, io, s), _t2(env, io, s), check_ms);
         });
 }
 
diff --git a/src/tests/library/tactic/tactic.cpp b/src/tests/library/tactic/tactic.cpp
index 028a4bb1f6..8a456db9f0 100644
--- a/src/tests/library/tactic/tactic.cpp
+++ b/src/tests/library/tactic/tactic.cpp
@@ -17,18 +17,18 @@ Author: Leonardo de Moura
 using namespace lean;
 
 tactic loop_tactic() {
-    return mk_tactic([=](environment const &, io_state const &, proof_state const &) -> proof_state_seq {
+    return mk_simple_tactic([=](environment const &, io_state const &, proof_state const & s) -> proof_state {
             while (true) {
                 check_interrupted();
             }
-            return proof_state_seq();
+            return s;
         });
 }
 
 tactic set_tactic(std::atomic<bool> * flag) {
-    return mk_tactic([=](environment const &, io_state const &, proof_state const & s) -> proof_state_seq {
+    return mk_simple_tactic([=](environment const &, io_state const &, proof_state const & s) -> proof_state {
             *flag = true;
-            return to_proof_state_seq(s);
+            return s;
         });
 }
 
@@ -73,13 +73,15 @@ static void tst1() {
                           100),
                   env, io, ctx, q);
     lean_assert(!flag1);
+    std::cout << "Before nested try_for...\n";
     check_failure(orelse(try_for(try_for(loop_tactic(), 10000), 100),
                          set_tactic(&flag1)),
                   env, io, ctx, q);
     lean_assert(flag1);
+    std::cout << "Before parallel 3 parallel tactics...\n";
     std::cout << "proof 2: " << par(loop_tactic(), par(loop_tactic(), t)).solve(env, io, ctx, q) << "\n";
 #endif
-
+    std::cout << "Before hello1 and 2...\n";
     std::cout << "proof 2: " << orelse(then(repeat_at_most(append(trace_tactic("hello1"), trace_tactic("hello2")), 5), fail_tactic()),
                                        t).solve(env, io, ctx, q) << "\n";
     std::cout << "------------------\n";