diff --git a/src/library/blast/expr.cpp b/src/library/blast/expr.cpp index 14b462d42..dbb2feb0e 100644 --- a/src/library/blast/expr.cpp +++ b/src/library/blast/expr.cpp @@ -121,11 +121,18 @@ scope_hash_consing::~scope_hash_consing() { g_lref_array = reinterpret_cast(m_lref_array); } +#ifdef LEAN_DEBUG static bool is_cached(level const & l) { lean_assert(g_level_table); return g_level_table->find(l) != g_level_table->end(); } +static bool is_cached(expr const & l) { + lean_assert(g_expr_table); + return g_expr_table->find(l) != g_expr_table->end(); +} +#endif + static level cache(level const & l) { lean_assert(g_level_table); auto r = g_level_table->find(l); @@ -135,11 +142,6 @@ static level cache(level const & l) { return l; } -static bool is_cached(expr const & l) { - lean_assert(g_expr_table); - return g_expr_table->find(l) != g_expr_table->end(); -} - static expr cache(expr const & e) { lean_assert(g_expr_table); auto r = g_expr_table->find(e);