diff --git a/src/library/blast/options.cpp b/src/library/blast/options.cpp
index 957c13920..8745203a7 100644
--- a/src/library/blast/options.cpp
+++ b/src/library/blast/options.cpp
@@ -19,6 +19,9 @@ Author: Leonardo de Moura
 #ifndef LEAN_DEFAULT_BLAST_TRACE
 #define LEAN_DEFAULT_BLAST_TRACE false
 #endif
+#ifndef LEAN_DEFAULT_BLAST_SUBST
+#define LEAN_DEFAULT_BLAST_SUBST true
+#endif
 
 namespace lean {
 namespace blast {
@@ -27,6 +30,7 @@ static name * g_blast_max_depth    = nullptr;
 static name * g_blast_init_depth   = nullptr;
 static name * g_blast_inc_depth    = nullptr;
 static name * g_blast_trace        = nullptr;
+static name * g_blast_subst        = nullptr;
 
 unsigned get_blast_max_depth(options const & o) {
     return o.get_unsigned(*g_blast_max_depth, LEAN_DEFAULT_BLAST_MAX_DEPTH);
@@ -40,12 +44,16 @@ unsigned get_blast_inc_depth(options const & o) {
 bool get_blast_trace(options const & o) {
     return o.get_bool(*g_blast_trace, LEAN_DEFAULT_BLAST_TRACE);
 }
+bool get_blast_subst(options const & o) {
+    return o.get_bool(*g_blast_subst, LEAN_DEFAULT_BLAST_SUBST);
+}
 
 config::config(options const & o) {
     m_max_depth  = get_blast_max_depth(o);
     m_init_depth = get_blast_init_depth(o);
     m_inc_depth  = get_blast_inc_depth(o);
     m_trace      = get_blast_trace(o);
+    m_subst      = get_blast_subst(o);
 }
 
 LEAN_THREAD_PTR(config, g_config);
@@ -70,6 +78,7 @@ void initialize_options() {
     g_blast_init_depth = new name{"blast", "init_depth"};
     g_blast_inc_depth  = new name{"blast", "inc_depth"};
     g_blast_trace      = new name{"blast", "trace"};
+    g_blast_subst      = new name{"blast", "subst"};
 
     register_unsigned_option(*blast::g_blast_max_depth, LEAN_DEFAULT_BLAST_MAX_DEPTH,
                              "(blast) max search depth for blast");
@@ -79,11 +88,14 @@ void initialize_options() {
                              "(blast) search depth increment for blast (remark: blast uses iteration deepening)");
     register_bool_option(*blast::g_blast_trace, LEAN_DEFAULT_BLAST_TRACE,
                          "(blast) trace");
+    register_bool_option(*blast::g_blast_subst, LEAN_DEFAULT_BLAST_SUBST,
+                         "(blast) enable subst action");
 }
 void finalize_options() {
     delete g_blast_max_depth;
     delete g_blast_init_depth;
     delete g_blast_inc_depth;
     delete g_blast_trace;
+    delete g_blast_subst;
 }
 }}
diff --git a/src/library/blast/options.h b/src/library/blast/options.h
index 69cf768ee..e4e504424 100644
--- a/src/library/blast/options.h
+++ b/src/library/blast/options.h
@@ -15,6 +15,7 @@ struct config {
     unsigned                   m_init_depth;
     unsigned                   m_inc_depth;
     bool                       m_trace;
+    bool                       m_subst;
     config(options const & o);
 };
 
diff --git a/src/library/blast/subst_action.cpp b/src/library/blast/subst_action.cpp
index 0280e73ad..f82bc5c17 100644
--- a/src/library/blast/subst_action.cpp
+++ b/src/library/blast/subst_action.cpp
@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "library/blast/intros_action.h"
 #include "library/blast/blast.h"
 #include "library/blast/trace.h"
+#include "library/blast/options.h"
 
 namespace lean {
 namespace blast {
@@ -86,6 +87,8 @@ bool subst_core(hypothesis_idx hidx) {
 }
 
 action_result subst_action(hypothesis_idx hidx) {
+    if (!get_config().m_subst)
+        return action_result::failed();
     state & s       = curr_state();
     app_builder & b = get_app_builder();
     hypothesis const & h = s.get_hypothesis_decl(hidx);