diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp
index 39b89077a..ee2d74a69 100644
--- a/src/library/tactic/tactic.cpp
+++ b/src/library/tactic/tactic.cpp
@@ -131,13 +131,13 @@ tactic try_for(tactic t, unsigned ms, unsigned check_ms) {
             try {
                 auto start = std::chrono::steady_clock::now();
                 std::chrono::milliseconds d(ms);
-                std::chrono::milliseconds one(1);
+                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(one);
+                    std::this_thread::sleep_for(small);
                 }
                 th.request_interrupt();
                 th.join();
diff --git a/src/library/tactic/tactic.h b/src/library/tactic/tactic.h
index cebd74713..35b9e69c0 100644
--- a/src/library/tactic/tactic.h
+++ b/src/library/tactic/tactic.h
@@ -9,7 +9,6 @@ Author: Leonardo de Moura
 #include <utility>
 #include <memory>
 #include <mutex>
-#include "util/interrupt.h"
 #include "util/lazy_list.h"
 #include "library/io_state.h"
 #include "library/tactic/proof_state.h"
@@ -63,6 +62,6 @@ tactic now_tactic();
 tactic assumption_tactic();
 tactic then(tactic t1, tactic t2);
 tactic orelse(tactic t1, tactic t2);
-tactic try_for(tactic t, unsigned ms, unsigned check_ms = g_small_sleep);
+tactic try_for(tactic t, unsigned ms, unsigned check_ms = 1);
 tactic repeat(tactic t1);
 }