From f1a244b858080c53ef3e4d3ea8bb7683e87cf07e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 19 Sep 2016 15:45:58 -0700
Subject: [PATCH] fix(frontends/lean/decl_util): bug at add_local_ref

---
 src/frontends/lean/decl_util.cpp | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/frontends/lean/decl_util.cpp b/src/frontends/lean/decl_util.cpp
index fc93765b1c..79f31d666a 100644
--- a/src/frontends/lean/decl_util.cpp
+++ b/src/frontends/lean/decl_util.cpp
@@ -275,7 +275,6 @@ void elaborate_params(elaborator & elab, buffer<expr> const & params, buffer<exp
 }
 
 environment add_local_ref(parser & p, environment const & env, name const & c_name, name const & c_real_name, buffer<name> const & lp_names, buffer<expr> const & var_params) {
-    if (!p.has_params()) return env;
     buffer<expr> params;
     buffer<name> lps;
     for (name const & u : lp_names) {