From a18c508f5c1f55fce2bd885eb7429e482f5dffa9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 22 Jun 2018 14:39:46 -0700
Subject: [PATCH] chore(kernel/old_type_checker): fix test

---
 src/kernel/old_type_checker.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/kernel/old_type_checker.cpp b/src/kernel/old_type_checker.cpp
index 670d3843c3..e33afc7a18 100644
--- a/src/kernel/old_type_checker.cpp
+++ b/src/kernel/old_type_checker.cpp
@@ -204,7 +204,7 @@ expr old_type_checker::infer_type_core(expr const & e, bool infer_only) {
     expr r;
     switch (e.kind()) {
     case expr_kind::FVar: r = local_type(e);  break;
-    case expr_kind::MVar: throw kernel_exception(m_env, "kernel type checker does not support meta variables");
+    case expr_kind::MVar: r = mvar_type(e); break;
     case expr_kind::BVar:
         lean_unreachable();  // LCOV_EXCL_LINE
     case expr_kind::Sort: