diff --git a/src/library/tactic/intro_tactic.cpp b/src/library/tactic/intro_tactic.cpp
index 2c721398dd..f287429342 100644
--- a/src/library/tactic/intro_tactic.cpp
+++ b/src/library/tactic/intro_tactic.cpp
@@ -87,6 +87,12 @@ optional<expr> intron(environment const & env, options const & opts, metavar_con
     return intron(env, opts, mctx, mvar, n, empty);
 }
 
+optional<expr> intron(environment const & env, options const & opts, metavar_context & mctx,
+                      expr const & mvar, unsigned n, buffer<name> & new_Hns) {
+    list<name> empty;
+    return intron(env, opts, mctx, mvar, n, empty, new_Hns);
+}
+
 optional<tactic_state> intron(unsigned n, tactic_state const & s, buffer<name> & new_Hns) {
     if (n == 0) return some_tactic_state(s);
     optional<expr> mvar  = s.get_main_goal();
diff --git a/src/library/tactic/intro_tactic.h b/src/library/tactic/intro_tactic.h
index 96bca0db6c..68bb09db7e 100644
--- a/src/library/tactic/intro_tactic.h
+++ b/src/library/tactic/intro_tactic.h
@@ -18,6 +18,8 @@ optional<expr> intron(environment const & env, options const & opts, metavar_con
                       expr const & mvar, unsigned n, list<name> & new_hs_names, buffer<name> & new_Hns);
 optional<expr> intron(environment const & env, options const & opts, metavar_context & mctx,
                       expr const & mvar, unsigned n, list<name> & new_hs_names);
+optional<expr> intron(environment const & env, options const & opts, metavar_context & mctx,
+                      expr const & mvar, unsigned n, buffer<name> & new_Hns);
 optional<expr> intron(environment const & env, options const & opts, metavar_context & mctx,
                       expr const & mvar, unsigned n);