From d4e410162b46fb4f37d8014656fe1a62c19cfbff Mon Sep 17 00:00:00 2001
From: Daniel Selsam <daniel.selsam@gmail.com>
Date: Fri, 6 Nov 2015 21:29:20 -0800
Subject: [PATCH] feat(library/blast/simplifier): expand macros

---
 src/library/blast/simplifier.cpp | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/library/blast/simplifier.cpp b/src/library/blast/simplifier.cpp
index cfc7811809..3d3d592197 100644
--- a/src/library/blast/simplifier.cpp
+++ b/src/library/blast/simplifier.cpp
@@ -276,11 +276,9 @@ result simplifier::simplify(expr const & e) {
     case expr_kind::Var:
         lean_unreachable();
     case expr_kind::Macro:
-        /* TODO
         if (m_expand_macros) {
-            if (auto m = blast::expand_macro(e)) r = join(r,simplify(whnf(*m)));
+            if (auto m = m_tmp_tctx->expand_macro(e)) r = join(r,simplify(whnf(*m)));
         }
-        */
         break;
     case expr_kind::Lambda:
         if (using_eq()) r = join(r,simplify_lambda(r.get_new()));