diff --git a/src/kernel/replace_visitor.h b/src/kernel/replace_visitor.h index a0dd57608c..bfe389e2ea 100644 --- a/src/kernel/replace_visitor.h +++ b/src/kernel/replace_visitor.h @@ -16,7 +16,7 @@ namespace lean { */ class replace_visitor { protected: - typedef expr_map cache; + typedef expr_bi_struct_map cache; cache m_cache; expr save_result(expr const & e, expr && r, bool shared); virtual expr visit_sort(expr const &);