From 28796593e3424f6d130ff96422ce8a2aefb83ce1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 25 Sep 2014 12:24:14 -0700
Subject: [PATCH] fix(kernel/type_checker): bug in new is_opaque method

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

diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index ccdd2eebb..dd0a161c0 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -414,7 +414,7 @@ bool type_checker::is_opaque(declaration const & d) const {
 bool type_checker::is_opaque(expr const & c) const {
     lean_assert(is_constant(c));
     if (auto d = m_env.find(const_name(c)))
-        return is_opaque(*d);
+        return d->is_definition() && is_opaque(*d);
     else
         return true;
 }