diff --git a/src/frontends/lean/frontend.h b/src/frontends/lean/frontend.h
index 98d3b38b4..b6dc62b77 100644
--- a/src/frontends/lean/frontend.h
+++ b/src/frontends/lean/frontend.h
@@ -189,13 +189,5 @@ public:
     void set_regular_channel(std::shared_ptr<output_channel> const & out) { m_state.set_regular_channel(out); }
     void set_diagnostic_channel(std::shared_ptr<output_channel> const & out) { m_state.set_diagnostic_channel(out); }
     /*@}*/
-
-    /**
-       @name Interrupts.
-    */
-    void set_interrupt(bool flag) { m_env.set_interrupt(flag); m_state.set_interrupt(flag); }
-    void interrupt() { set_interrupt(true); }
-    void reset_interrupt() { set_interrupt(false); }
-    /*@}*/
 };
 }
diff --git a/src/frontends/lean/frontend_elaborator.cpp b/src/frontends/lean/frontend_elaborator.cpp
index 4d4cfa17c..d1b0eaec6 100644
--- a/src/frontends/lean/frontend_elaborator.cpp
+++ b/src/frontends/lean/frontend_elaborator.cpp
@@ -8,7 +8,7 @@ Author: Leonardo de Moura
 #include <utility>
 #include <algorithm>
 #include <limits>
-#include "util/interruptable_ptr.h"
+#include "util/interrupt.h"
 #include "kernel/type_checker.h"
 #include "kernel/type_checker_justification.h"
 #include "kernel/normalizer.h"
@@ -112,8 +112,6 @@ class frontend_elaborator::imp {
     // We need that because a frontend may associate line number information
     // with the original non-elaborated expressions.
     expr_map<expr>                      m_trace;
-    interruptable_ptr<elaborator>       m_elaborator;
-    volatile bool                       m_interrupted;
 
     /**
        \brief Replace placeholders and choices with metavariables.
@@ -378,7 +376,7 @@ class frontend_elaborator::imp {
         }
 
         virtual expr visit(expr const & e, context const & ctx) {
-            check_interrupted(m_ref.m_interrupted);
+            check_interrupted();
             expr r = replace_visitor::visit(e, ctx);
             if (!is_eqp(r, e))
                 m_ref.m_trace[r] = e;
@@ -392,7 +390,6 @@ class frontend_elaborator::imp {
         //                     return !is_choice(c1) && is_choice(c2);
         //                 });
         elaborator elb(m_env, m_menv, m_ucs.size(), m_ucs.data());
-        scoped_set_interruptable_ptr<elaborator> set(m_elaborator, &elb);
         return elb.next();
     }
 
@@ -403,7 +400,6 @@ public:
         m_type_checker(m_env),
         m_type_inferer(m_env),
         m_normalizer(m_env) {
-        m_interrupted = false;
     }
 
     expr elaborate(expr const & e) {
@@ -458,14 +454,6 @@ public:
         }
     }
 
-    void set_interrupt(bool f) {
-        m_interrupted = f;
-        m_type_checker.set_interrupt(f);
-        m_type_inferer.set_interrupt(f);
-        m_normalizer.set_interrupt(f);
-        m_elaborator.set_interrupt(f);
-    }
-
     void clear() {
         m_menv = metavar_env();
         m_ucs.clear();
@@ -485,7 +473,6 @@ frontend_elaborator::~frontend_elaborator() {}
 expr frontend_elaborator::operator()(expr const & e) { return m_ptr->elaborate(e); }
 std::pair<expr, expr> frontend_elaborator::operator()(name const & n, expr const & t, expr const & e) { return m_ptr->elaborate(n, t, e); }
 expr const & frontend_elaborator::get_original(expr const & e) const { return m_ptr->get_original(e); }
-void frontend_elaborator::set_interrupt(bool f) { m_ptr->set_interrupt(f); }
 void frontend_elaborator::clear() { m_ptr->clear(); }
 environment const & frontend_elaborator::get_environment() const { return m_ptr->get_environment(); }
 }
diff --git a/src/frontends/lean/frontend_elaborator.h b/src/frontends/lean/frontend_elaborator.h
index 19d81556d..3f22055c9 100644
--- a/src/frontends/lean/frontend_elaborator.h
+++ b/src/frontends/lean/frontend_elaborator.h
@@ -44,10 +44,6 @@ public:
     */
     expr const & get_original(expr const & e) const;
 
-    void set_interrupt(bool flag);
-    void interrupt() { set_interrupt(true); }
-    void reset_interrupt() { set_interrupt(false); }
-
     void clear();
 
     environment const & get_environment() const;
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 6de369ea4..b1014f7a7 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -20,6 +20,7 @@ Author: Leonardo de Moura
 #include "util/exception.h"
 #include "util/sstream.h"
 #include "util/sexpr/option_declarations.h"
+#include "util/interrupt.h"
 #include "kernel/normalizer.h"
 #include "kernel/type_checker.h"
 #include "kernel/free_vars.h"
@@ -129,10 +130,6 @@ class parser::imp {
     expr_pos_info       m_expr_pos_info;
     pos_info            m_last_cmd_pos;
     pos_info            m_last_script_pos;
-    // Reference to temporary parser used to process import command.
-    // We need this reference to be able to interrupt it.
-    interruptable_ptr<parser>     m_import_parser;
-    interruptable_ptr<normalizer> m_normalizer;
 
     leanlua_state *     m_leanlua_state;
 
@@ -1170,7 +1167,6 @@ class parser::imp {
         next();
         expr v = m_elaborator(parse_expr());
         normalizer norm(m_frontend);
-        scoped_set_interruptable_ptr<normalizer> set(m_normalizer, &norm);
         expr r = norm(v);
         regular(m_frontend) << r << endl;
     }
@@ -1403,7 +1399,6 @@ class parser::imp {
             if (m_verbose)
                 regular(m_frontend) << "Importing file '" << fname << "'" << endl;
             parser import_parser(m_frontend, in, m_leanlua_state, true /* use exceptions */, false /* not interactive */);
-            scoped_set_interruptable_ptr<parser> set(m_import_parser, &import_parser);
             import_parser();
         } catch (interrupted &) {
             throw;
@@ -1686,17 +1681,6 @@ public:
             throw parser_exception(ex.what(), ex.m_pos.first, ex.m_pos.second);
         }
     }
-
-    void set_interrupt(bool flag) {
-        m_frontend.set_interrupt(flag);
-        m_elaborator.set_interrupt(flag);
-        m_import_parser.set_interrupt(flag);
-        m_normalizer.set_interrupt(flag);
-    }
-
-    void reset_interrupt() {
-        set_interrupt(false);
-    }
 };
 
 parser::parser(frontend & fe, std::istream & in, leanlua_state * S, bool use_exceptions, bool interactive) {
@@ -1711,10 +1695,6 @@ bool parser::operator()() {
     return m_ptr->parse_commands();
 }
 
-void parser::set_interrupt(bool flag) {
-    m_ptr->set_interrupt(flag);
-}
-
 expr parser::parse_expr() {
     return m_ptr->parse_expr_main();
 }
@@ -1736,7 +1716,6 @@ bool shell::operator()() {
         std::istringstream strm(input);
         {
             parser p(m_frontend, strm, m_leanlua_state, false, false);
-            scoped_set_interruptable_ptr<parser> set(m_parser, &p);
             if (!p())
                 errors = true;
         }
@@ -1744,12 +1723,7 @@ bool shell::operator()() {
     }
 #else
     parser p(m_frontend, std::cin, m_leanlua_state, false, true);
-    scoped_set_interruptable_ptr<parser> set(m_parser, &p);
     return p();
 #endif
 }
-
-void shell::set_interrupt(bool flag) {
-    m_parser.set_interrupt(flag);
-}
 }
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index 061724dee..174b9029d 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -6,7 +6,6 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <iostream>
-#include "util/interruptable_ptr.h"
 #include "frontends/lean/frontend.h"
 
 namespace lean {
@@ -24,26 +23,17 @@ public:
 
     /** \brief Parse a single expression */
     expr parse_expr();
-
-    void set_interrupt(bool flag);
-    void interrupt() { set_interrupt(true); }
-    void reset_interrupt() { set_interrupt(false); }
 };
 
 /** \brief Implements the Read Eval Print loop */
 class shell {
     frontend &                m_frontend;
     leanlua_state *           m_leanlua_state;
-    interruptable_ptr<parser> m_parser;
 public:
     shell(frontend & fe, leanlua_state * S);
     ~shell();
 
     bool operator()();
-
-    void set_interrupt(bool flag);
-    void interrupt() { set_interrupt(true); }
-    void reset_interrupt() { set_interrupt(false); }
 };
 
 inline bool parse_commands(frontend & fe, std::istream & in, leanlua_state * S = nullptr, bool use_exceptions = true, bool interactive = false) {
diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index f41a0ce5c..07d5a044c 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -13,7 +13,7 @@ Author: Leonardo de Moura
 #include "util/exception.h"
 #include "util/scoped_set.h"
 #include "util/sexpr/options.h"
-#include "util/interruptable_ptr.h"
+#include "util/interrupt.h"
 #include "kernel/context.h"
 #include "kernel/for_each.h"
 #include "kernel/occurs.h"
@@ -169,8 +169,6 @@ class pp_fn {
     bool             m_notation;         //!< if true use notation
     bool             m_extra_lets;       //!< introduce extra let-expression to cope with sharing.
     unsigned         m_alias_min_weight; //!< minimal weight for creating an alias
-    volatile bool    m_interrupted;
-
 
     // Create a scope for local definitions
     struct mk_scope {
@@ -1072,7 +1070,7 @@ class pp_fn {
     }
 
     result pp(expr const & e, unsigned depth, bool main = false) {
-        check_interrupted(m_interrupted);
+        check_interrupted();
         if (!is_atomic(e) && (m_num_steps > m_max_steps || depth > m_max_depth)) {
             return pp_ellipsis();
         } else {
@@ -1170,7 +1168,6 @@ public:
     pp_fn(frontend const & fe, options const & opts):
         m_frontend(fe) {
         set_options(opts);
-        m_interrupted = false;
         m_num_steps   = 0;
     }
 
@@ -1190,10 +1187,6 @@ public:
         return pp_abstraction_core(e, 0, expr(), &implicit_args).first;
     }
 
-    void set_interrupt(bool flag) {
-        m_interrupted = flag;
-    }
-
     void register_local(name const & n) {
         m_local_names.insert(n);
     }
@@ -1201,24 +1194,20 @@ public:
 
 class pp_formatter_cell : public formatter_cell {
     frontend const &         m_frontend;
-    interruptable_ptr<pp_fn> m_pp_fn;
-    volatile bool            m_interrupted;
 
     format pp(expr const & e, options const & opts) {
         pp_fn fn(m_frontend, opts);
-        scoped_set_interruptable_ptr<pp_fn> set(m_pp_fn, &fn);
         return fn(e);
     }
 
     format pp(context const & c, expr const & e, bool include_e, options const & opts) {
         pp_fn fn(m_frontend, opts);
-        scoped_set_interruptable_ptr<pp_fn> set(m_pp_fn, &fn);
         unsigned indent = get_pp_indent(opts);
         format r;
         bool first = true;
         expr c2   = context_to_lambda(c, e);
         while (is_fake_context(c2)) {
-            check_interrupted(m_interrupted);
+            check_interrupted();
             name n1 = get_unused_name(c2);
             fn.register_local(n1);
             format entry = format{format(n1), space(), colon(), space(), fn(fake_context_domain(c2))};
@@ -1255,7 +1244,7 @@ class pp_formatter_cell : public formatter_cell {
         expr it1 = t;
         expr it2 = v;
         while (is_pi(it1) && is_lambda(it2)) {
-            check_interrupted(m_interrupted);
+            check_interrupted();
             if (abst_domain(it1) != abst_domain(it2))
                 return pp_definition(kwd, n, t, v, opts);
             it1 = abst_body(it1);
@@ -1269,7 +1258,6 @@ class pp_formatter_cell : public formatter_cell {
             if (m_frontend.has_implicit_arguments(n))
                 implicit_args = &(m_frontend.get_implicit_arguments(n));
             pp_fn fn(m_frontend, opts);
-            scoped_set_interruptable_ptr<pp_fn> set(m_pp_fn, &fn);
             format def = fn.pp_definition(v, t, implicit_args);
             return format{highlight_command(format(kwd)), space(), format(n), def};
         }
@@ -1286,7 +1274,6 @@ class pp_formatter_cell : public formatter_cell {
         format r = format{highlight_command(format(kwd)), space(), format(n)};
         if (m_frontend.has_implicit_arguments(n)) {
             pp_fn fn(m_frontend, opts);
-            scoped_set_interruptable_ptr<pp_fn> set(m_pp_fn, &fn);
             r += fn.pp_pi_with_implicit_args(obj.get_type(), m_frontend.get_implicit_arguments(n));
         } else {
             r += format{space(), colon(), space(), pp(obj.get_type(), opts)};
@@ -1329,7 +1316,6 @@ class pp_formatter_cell : public formatter_cell {
 public:
     pp_formatter_cell(frontend const & fe):
         m_frontend(fe) {
-        m_interrupted = false;
     }
 
     virtual ~pp_formatter_cell() {
@@ -1348,10 +1334,9 @@ public:
             return pp(c, e, true, opts);
         } else {
             pp_fn fn(m_frontend, opts);
-            scoped_set_interruptable_ptr<pp_fn> set(m_pp_fn, &fn);
             expr c2   = context_to_lambda(c, e);
             while (is_fake_context(c2)) {
-                check_interrupted(m_interrupted);
+                check_interrupted();
                 name n1 = get_unused_name(c2);
                 fn.register_local(n1);
                 expr const & rest = fake_context_rest(c2);
@@ -1389,17 +1374,12 @@ public:
         std::for_each(env.begin_objects(),
                       env.end_objects(),
                       [&](object const & obj) {
-                          check_interrupted(m_interrupted);
+                          check_interrupted();
                           if (first) first = false; else r += line();
                           r += operator()(obj, opts);
                       });
         return r;
     }
-
-    virtual void set_interrupt(bool flag) {
-        m_pp_fn.set_interrupt(flag);
-        m_interrupted = flag;
-    }
 };
 
 formatter mk_pp_formatter(frontend const & fe) {
diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp
index 39046d293..02b7e0048 100644
--- a/src/kernel/environment.cpp
+++ b/src/kernel/environment.cpp
@@ -402,10 +402,6 @@ struct environment::imp {
         }
     }
 
-    void set_interrupt(bool flag) {
-        m_type_checker->set_interrupt(flag);
-    }
-
     imp():
         m_num_children(0) {
         init_uvars();
@@ -531,10 +527,6 @@ void environment::display(std::ostream & out) const {
     m_ptr->display(out, *this);
 }
 
-void environment::set_interrupt(bool flag) {
-    m_ptr->set_interrupt(flag);
-}
-
 environment::extension const & environment::get_extension_core(unsigned extid) const {
     return m_ptr->get_extension_core(extid);
 }
diff --git a/src/kernel/environment.h b/src/kernel/environment.h
index a4004d0e1..10a1f43c7 100644
--- a/src/kernel/environment.h
+++ b/src/kernel/environment.h
@@ -209,10 +209,6 @@ public:
     /** \brief Display universal variable constraints and objects stored in this environment and its parents. */
     void display(std::ostream & out) const;
 
-    void set_interrupt(bool flag);
-    void interrupt() { set_interrupt(true); }
-    void reset_interrupt() { set_interrupt(false); }
-
     /**
        \brief Frontend can store data in environment extensions.
        Each extension is associated with a unique token/id.
diff --git a/src/kernel/formatter.h b/src/kernel/formatter.h
index 2a8c34251..3d90f2b4f 100644
--- a/src/kernel/formatter.h
+++ b/src/kernel/formatter.h
@@ -34,8 +34,6 @@ public:
     virtual format operator()(object const & obj, options const & opts) = 0;
     /** \brief Format the given environment */
     virtual format operator()(environment const & env, options const & opts) = 0;
-    /** \brief Request interruption */
-    virtual void set_interrupt(bool ) {}
 };
 /**
    \brief Smart-pointer for the actual formatter object (aka \c formatter_cell).
@@ -50,7 +48,6 @@ public:
     format operator()(context const & c, expr const & e, bool format_ctx = false, options const & opts = options()) const { return (*m_cell)(c, e, format_ctx, opts); }
     format operator()(object const & obj, options const & opts = options()) const { return (*m_cell)(obj, opts); }
     format operator()(environment const & env, options const & opts = options()) const { return (*m_cell)(env, opts); }
-    void set_interrupt(bool flag) { m_cell->set_interrupt(flag); }
 };
 /**
    \brief Create a simple formatter object based on \c print function.
diff --git a/src/kernel/normalizer.cpp b/src/kernel/normalizer.cpp
index 34705fd7b..0aefcc8b7 100644
--- a/src/kernel/normalizer.cpp
+++ b/src/kernel/normalizer.cpp
@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "util/list.h"
 #include "util/flet.h"
 #include "util/buffer.h"
+#include "util/interrupt.h"
 #include "util/sexpr/options.h"
 #include "kernel/normalizer.h"
 #include "kernel/expr.h"
@@ -74,7 +75,6 @@ class normalizer::imp {
     cache                 m_cache;
     unsigned              m_max_depth;
     unsigned              m_depth;
-    volatile bool         m_interrupted;
 
     environment env() const { return environment(m_env); }
 
@@ -179,7 +179,7 @@ class normalizer::imp {
     /** \brief Normalize the expression \c a in a context composed of stack \c s and \c k binders. */
     svalue normalize(expr const & a, value_stack const & s, unsigned k) {
         flet<unsigned> l(m_depth, m_depth+1);
-        check_interrupted(m_interrupted);
+        check_interrupted();
         if (m_depth > m_max_depth)
             throw kernel_exception(env(), "normalizer maximum recursion depth exceeded");
         bool shared = false;
@@ -294,7 +294,6 @@ class normalizer::imp {
 public:
     imp(environment const & env, unsigned max_depth):
         m_env(env.to_weak_ref()) {
-        m_interrupted    = false;
         m_max_depth      = max_depth;
         m_depth          = 0;
     }
@@ -306,7 +305,6 @@ public:
     }
 
     void clear() { m_ctx = context(); m_cache.clear(); }
-    void set_interrupt(bool flag) { m_interrupted = flag; }
 };
 
 normalizer::normalizer(environment const & env, unsigned max_depth):m_ptr(new imp(env, max_depth)) {}
@@ -315,7 +313,6 @@ normalizer::normalizer(environment const & env, options const & opts):normalizer
 normalizer::~normalizer() {}
 expr normalizer::operator()(expr const & e, context const & ctx) { return (*m_ptr)(e, ctx); }
 void normalizer::clear() { m_ptr->clear(); }
-void normalizer::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); }
 
 expr normalize(expr const & e, environment const & env, context const & ctx) {
     return normalizer(env)(e, ctx);
diff --git a/src/kernel/normalizer.h b/src/kernel/normalizer.h
index bb76ae9ba..b7842f3b8 100644
--- a/src/kernel/normalizer.h
+++ b/src/kernel/normalizer.h
@@ -26,10 +26,6 @@ public:
     expr operator()(expr const & e, context const & ctx = context());
 
     void clear();
-
-    void set_interrupt(bool flag);
-    void interrupt() { set_interrupt(true); }
-    void reset_interrupt() { set_interrupt(false); }
 };
 /** \brief Normalize \c e using the environment \c env and context \c ctx */
 expr normalize(expr const & e, environment const & env, context const & ctx = context());
diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index d261a1ec0..d6a8cafe6 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include "util/scoped_map.h"
 #include "util/flet.h"
+#include "util/interrupt.h"
 #include "kernel/type_checker.h"
 #include "kernel/environment.h"
 #include "kernel/kernel_exception.h"
@@ -29,7 +30,6 @@ class type_checker::imp {
     metavar_env *             m_menv;
     unsigned                  m_menv_timestamp;
     unification_constraints * m_uc;
-    volatile bool             m_interrupted;
 
     environment env() const {
         return environment(m_env);
@@ -85,7 +85,7 @@ class type_checker::imp {
     }
 
     expr infer_type_core(expr const & e, context const & ctx) {
-        check_interrupted(m_interrupted);
+        check_interrupted();
         bool shared = false;
         if (is_shared(e)) {
             shared = true;
@@ -289,7 +289,6 @@ public:
         m_menv           = nullptr;
         m_menv_timestamp = 0;
         m_uc              = nullptr;
-        m_interrupted     = false;
     }
 
     expr infer_type(expr const & e, context const & ctx, metavar_env * menv, buffer<unification_constraint> & uc) {
@@ -315,11 +314,6 @@ public:
         check_type(t, e, ctx);
     }
 
-    void set_interrupt(bool flag) {
-        m_interrupted = flag;
-        m_normalizer.set_interrupt(flag);
-    }
-
     void clear() {
         m_cache.clear();
         m_normalizer.clear();
@@ -349,7 +343,6 @@ void type_checker::check_type(expr const & e, context const & ctx) {
     m_ptr->check_type(e, ctx);
 }
 void type_checker::clear() { m_ptr->clear(); }
-void type_checker::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); }
 normalizer & type_checker::get_normalizer() { return m_ptr->get_normalizer(); }
 
 expr  infer_type(expr const & e, environment const & env, context const & ctx) {
diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h
index 23e599220..b208f54c0 100644
--- a/src/kernel/type_checker.h
+++ b/src/kernel/type_checker.h
@@ -56,11 +56,6 @@ public:
     /** \brief Reset internal caches */
     void clear();
 
-    /** \brief Interrupt type checker */
-    void set_interrupt(bool flag);
-    void interrupt() { set_interrupt(true); }
-    void reset_interrupt() { set_interrupt(false); }
-
     /** \brief Return reference to the normalizer used by this type checker. */
     normalizer & get_normalizer();
 };
diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp
index f2f2eb579..f6e2afa95 100644
--- a/src/library/elaborator/elaborator.cpp
+++ b/src/library/elaborator/elaborator.cpp
@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include <vector>
 #include <utility>
 #include "util/pdeque.h"
+#include "util/interrupt.h"
 #include "kernel/formatter.h"
 #include "kernel/free_vars.h"
 #include "kernel/normalizer.h"
@@ -143,8 +144,6 @@ class elaborator::imp {
     int                                      m_quota;
     justification                            m_conflict;
     bool                                     m_first;
-    bool                                     m_interrupted;
-
 
     // options
     bool                                     m_use_justifications;
@@ -596,7 +595,7 @@ class elaborator::imp {
         context const & ctx = get_context(c);
         bool modified = false;
         while (true) {
-            check_interrupted(m_interrupted);
+            check_interrupted();
             expr new_a = normalize_step(ctx, a);
             expr new_b = normalize_step(ctx, b);
             if (new_a == a && new_b == b) {
@@ -1380,13 +1379,12 @@ public:
         set_options(opts);
         m_next_id     = 0;
         m_quota       = 0;
-        m_interrupted = false;
         m_first       = true;
         // display(std::cout);
     }
 
     metavar_env next() {
-        check_interrupted(m_interrupted);
+        check_interrupted();
         if (m_conflict)
             throw elaborator_exception(m_conflict);
         if (!m_case_splits.empty()) {
@@ -1404,7 +1402,7 @@ public:
         }
         reset_quota();
         while (true) {
-            check_interrupted(m_interrupted);
+            check_interrupted();
             cnstr_queue & q = m_state.m_queue;
             if (q.empty() || m_quota < - static_cast<int>(q.size()) - 10) {
                 // TODO(Leo): implement interface with synthesizer
@@ -1420,12 +1418,6 @@ public:
         }
     }
 
-    void interrupt() {
-        m_interrupted = true;
-        m_type_inferer.set_interrupt(true);
-        m_normalizer.set_interrupt(true);
-    }
-
     void display(std::ostream & out, unification_constraint const & c) const {
         formatter fmt = mk_simple_formatter();
         out << c.pp(fmt, options(), nullptr, false) << "\n";
@@ -1462,8 +1454,4 @@ elaborator::~elaborator() {
 metavar_env elaborator::next() {
     return m_ptr->next();
 }
-
-void elaborator::interrupt() {
-    m_ptr->interrupt();
-}
 }
diff --git a/src/library/elaborator/elaborator.h b/src/library/elaborator/elaborator.h
index 034162d6d..ded5fd124 100644
--- a/src/library/elaborator/elaborator.h
+++ b/src/library/elaborator/elaborator.h
@@ -61,7 +61,5 @@ public:
     ~elaborator();
 
     metavar_env next();
-    void interrupt();
-    void set_interrupt(bool ) { interrupt(); }
 };
 }
diff --git a/src/library/elaborator/elaborator_plugin.h b/src/library/elaborator/elaborator_plugin.h
index 60273b305..427971e3b 100644
--- a/src/library/elaborator/elaborator_plugin.h
+++ b/src/library/elaborator/elaborator_plugin.h
@@ -29,7 +29,6 @@ public:
         */
         virtual std::pair<metavar_env, list<unification_constraint>> next(justification const & assumption) = 0;
         /** \brief Interrupt the computation for the next solution. */
-        virtual void interrupt() = 0;
     };
 
     /**
diff --git a/src/library/elaborator/synthesizer.h b/src/library/elaborator/synthesizer.h
index 197ba128d..fccccb0f3 100644
--- a/src/library/elaborator/synthesizer.h
+++ b/src/library/elaborator/synthesizer.h
@@ -25,7 +25,6 @@ public:
         /** \brief Return the next possible solution. An elaborator_exception is throw in case of failure. */
         virtual expr next() = 0;
         /** \brief Interrupt the computation for the next solution. */
-        virtual void interrupt() = 0;
     };
 
     /**
diff --git a/src/library/state.h b/src/library/state.h
index 017257f51..3a6a51243 100644
--- a/src/library/state.h
+++ b/src/library/state.h
@@ -39,7 +39,6 @@ public:
     template<typename T> void set_option(name const & n, T const & v) {
         set_options(get_options().update(n, v));
     }
-    void set_interrupt(bool flag) { m_formatter.set_interrupt(flag); }
 };
 
 /**
diff --git a/src/library/type_inferer.cpp b/src/library/type_inferer.cpp
index 85a2b7fec..b0b5b793b 100644
--- a/src/library/type_inferer.cpp
+++ b/src/library/type_inferer.cpp
@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include "util/flet.h"
 #include "util/scoped_map.h"
+#include "util/interrupt.h"
 #include "kernel/environment.h"
 #include "kernel/normalizer.h"
 #include "kernel/builtin.h"
@@ -29,7 +30,6 @@ class type_inferer::imp {
     unification_constraints * m_uc;
     normalizer                m_normalizer;
     cache                     m_cache;
-    volatile bool             m_interrupted;
 
     expr normalize(expr const & e, context const & ctx) {
         return m_normalizer(e, ctx);
@@ -139,7 +139,7 @@ class type_inferer::imp {
             break; // expensive cases
         }
 
-        check_interrupted(m_interrupted);
+        check_interrupted();
         bool shared = false;
         if (is_shared(e)) {
             shared = true;
@@ -214,7 +214,6 @@ public:
     imp(environment const & env):
         m_env(env),
         m_normalizer(env) {
-        m_interrupted    = false;
         m_menv           = nullptr;
         m_menv_timestamp = 0;
         m_uc             = nullptr;
@@ -227,11 +226,6 @@ public:
         return infer_type(e, ctx);
     }
 
-    void set_interrupt(bool flag) {
-        m_interrupted = flag;
-        m_normalizer.set_interrupt(flag);
-    }
-
     void clear() {
         m_cache.clear();
         m_normalizer.clear();
@@ -250,5 +244,4 @@ expr type_inferer::operator()(expr const & e, context const & ctx) {
     return operator()(e, ctx, nullptr, uc);
 }
 void type_inferer::clear() { m_ptr->clear(); }
-void type_inferer::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); }
 }
diff --git a/src/library/type_inferer.h b/src/library/type_inferer.h
index 2c99900f5..0c948d149 100644
--- a/src/library/type_inferer.h
+++ b/src/library/type_inferer.h
@@ -35,9 +35,5 @@ public:
     expr operator()(expr const & e, context const & ctx = context());
 
     void clear();
-
-    void set_interrupt(bool flag);
-    void interrupt() { set_interrupt(true); }
-    void reset_interrupt() { set_interrupt(false); }
 };
 }
diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp
index 4ff702472..217c1d2e4 100644
--- a/src/shell/lean.cpp
+++ b/src/shell/lean.cpp
@@ -7,23 +7,19 @@ Author: Leonardo de Moura
 #include <iostream>
 #include <fstream>
 #include <signal.h>
-#include "util/interruptable_ptr.h"
+#include "util/interrupt.h"
 #include "kernel/printer.h"
 #include "frontends/lean/parser.h"
 #include "bindings/lua/leanlua_state.h"
 #include "version.h"
 
-using lean::interruptable_ptr;
 using lean::shell;
 using lean::frontend;
-using lean::scoped_set_interruptable_ptr;
 using lean::parser;
 using lean::leanlua_state;
 
-static interruptable_ptr<shell> g_lean_shell;
-
 static void on_ctrl_c(int ) {
-    g_lean_shell.set_interrupt(true);
+    lean::request_interrupt();
 }
 
 bool lean_shell() {
@@ -32,7 +28,6 @@ bool lean_shell() {
     frontend f;
     leanlua_state S;
     shell sh(f, &S);
-    scoped_set_interruptable_ptr<shell> set(g_lean_shell, &sh);
     signal(SIGINT, on_ctrl_c);
     return sh();
 }
diff --git a/src/tests/kernel/normalizer.cpp b/src/tests/kernel/normalizer.cpp
index 928bc8f6e..62382a4fe 100644
--- a/src/tests/kernel/normalizer.cpp
+++ b/src/tests/kernel/normalizer.cpp
@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "util/test.h"
 #include "util/trace.h"
 #include "util/exception.h"
+#include "util/interrupt.h"
 #include "kernel/normalizer.h"
 #include "kernel/builtin.h"
 #include "kernel/expr_sets.h"
@@ -219,7 +220,7 @@ static void tst5() {
     env.add_var("a", Bool);
     normalizer proc(env);
     std::chrono::milliseconds dura(50);
-    std::thread thread([&]() {
+    interruptible_thread thread([&]() {
             try {
                 proc(t);
                 // Remark: if the following code is reached, we
@@ -230,7 +231,8 @@ static void tst5() {
             }
         });
     std::this_thread::sleep_for(dura);
-    proc.interrupt();
+    while (!thread.request_interrupt()) {
+    }
     thread.join();
 #endif
 }
diff --git a/src/tests/kernel/type_checker.cpp b/src/tests/kernel/type_checker.cpp
index f41c232b8..6316b8952 100644
--- a/src/tests/kernel/type_checker.cpp
+++ b/src/tests/kernel/type_checker.cpp
@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "util/test.h"
 #include "util/trace.h"
 #include "util/exception.h"
+#include "util/interrupt.h"
 #include "kernel/type_checker.h"
 #include "kernel/environment.h"
 #include "kernel/abstract.h"
@@ -227,7 +228,7 @@ static void tst12() {
     env.add_var("a", Int);
     type_checker checker(env);
     std::chrono::milliseconds dura(100);
-    std::thread thread([&]() {
+    interruptible_thread thread([&]() {
             try {
                 std::cout << checker.infer_type(t) << "\n";
                 // Remark: if the following code is reached, we
@@ -238,7 +239,8 @@ static void tst12() {
             }
         });
     std::this_thread::sleep_for(dura);
-    checker.interrupt();
+    while (!thread.request_interrupt()) {
+    }
     thread.join();
 #endif
 }
diff --git a/src/tests/library/formatter.cpp b/src/tests/library/formatter.cpp
index 1f6b9a57a..6dd87cdd6 100644
--- a/src/tests/library/formatter.cpp
+++ b/src/tests/library/formatter.cpp
@@ -39,8 +39,6 @@ static void tst1() {
     check(fmt(ctx), "[x : f a; y : f x (N -> N); z : N := y == x]");
     check(fmt(ctx, f(Var(0), Var(2))), "f z x");
     check(fmt(ctx, f(Var(0), Var(2)), true), "[x : f a; y : f x (N -> N); z : N := y == x] |- f z x");
-    fmt.set_interrupt(true);
-    fmt.set_interrupt(false);
 }
 
 int main() {
diff --git a/src/util/interrupt.cpp b/src/util/interrupt.cpp
index 98a655cac..ff40ab125 100644
--- a/src/util/interrupt.cpp
+++ b/src/util/interrupt.cpp
@@ -18,12 +18,12 @@ void reset_interrupt() {
     g_interrupt.store(false);
 }
 
-bool interrupted() {
+bool interrupt_requested() {
     return g_interrupt.load();
 }
 
-void check_interrupt() {
-    if (interrupted())
+void check_interrupted() {
+    if (interrupt_requested())
         throw interrupted();
 }
 
diff --git a/src/util/interrupt.h b/src/util/interrupt.h
index 7f9cddb1e..c56bc6bec 100644
--- a/src/util/interrupt.h
+++ b/src/util/interrupt.h
@@ -22,12 +22,12 @@ void reset_interrupt();
 /**
    \brief Return true iff the current thread was marked for interruption.
 */
-bool interrupted();
+bool interrupt_requested();
 
 /**
-   \brief Throw an interrupt exception if the (interrupt) flag is set.
+   \brief Throw an interrupted exception if the (interrupt) flag is set.
 */
-void check_interrupt();
+void check_interrupted();
 
 /**
    \brief Thread that provides a method for setting its interrupt flag.