From e9d2d51760e40a8833e31e1f059e1f04295ce74e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 3 Aug 2016 18:43:55 -0700
Subject: [PATCH] fix(library/type_context): prevent assertion violation

---
 src/library/type_context.cpp | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index 3cdd378944..2e29916344 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -411,10 +411,12 @@ expr type_context::whnf_core(expr const & e) {
         /* Remark: we do not unfold Constants eagerly in this method */
         return e;
     case expr_kind::Local:
-        if (auto d = m_lctx.get_local_decl(e)) {
-            if (auto v = d->get_value()) {
-                /* zeta-reduction */
-                return whnf_core(*v);
+        if (is_local_decl_ref(e)) {
+            if (auto d = m_lctx.get_local_decl(e)) {
+                if (auto v = d->get_value()) {
+                    /* zeta-reduction */
+                    return whnf_core(*v);
+                }
             }
         }
         return e;