diff --git a/src/library/tactic/ac_tactics.cpp b/src/library/tactic/ac_tactics.cpp
index a0041f9780..321e3ea2f9 100644
--- a/src/library/tactic/ac_tactics.cpp
+++ b/src/library/tactic/ac_tactics.cpp
@@ -120,6 +120,10 @@ struct flat_assoc_fn {
     }
 };
 
+pair<expr, optional<expr>> flat_assoc(type_context & ctx, expr const & op, expr const & assoc, expr const & e) {
+    return flat_assoc_fn(ctx, op, assoc).flat_core(e);
+}
+
 #define TRY   LEAN_TACTIC_TRY
 #define CATCH LEAN_TACTIC_CATCH(to_tactic_state(s))
 
diff --git a/src/library/tactic/ac_tactics.h b/src/library/tactic/ac_tactics.h
index cee270a863..8766e69500 100644
--- a/src/library/tactic/ac_tactics.h
+++ b/src/library/tactic/ac_tactics.h
@@ -5,7 +5,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include "library/type_context.h"
+
 namespace lean {
+pair<expr, optional<expr>> flat_assoc(type_context & ctx, expr const & op, expr const & assoc, expr const & e);
 void initialize_ac_tactics();
 void finalize_ac_tactics();
 }