From 1e370023b1ce9033032e405fe549da3bda7a7b07 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 30 Aug 2013 13:25:30 -0700
Subject: [PATCH] Attach elaborator the lean default parser

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/lean_parser.cpp | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/frontends/lean/lean_parser.cpp b/src/frontends/lean/lean_parser.cpp
index 727b9bcd6..352c453dd 100644
--- a/src/frontends/lean/lean_parser.cpp
+++ b/src/frontends/lean/lean_parser.cpp
@@ -962,9 +962,9 @@ class parser::imp {
 
     expr elaborate(expr const & e) {
         if (has_metavar(e)) {
-            // TODO fix
-            regular(m_frontend) << e << endl;
-            throw parser_error("expression contains metavariables... not implemented yet.", m_last_cmd_pos);
+            expr r = m_elaborator(e);
+            m_elaborator.clear();
+            return r;
         } else {
             return e;
         }