From 092985f7774fbcf2e166d2365a680d4a6992b3f4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 28 Mar 2017 11:55:11 -0700
Subject: [PATCH] fix(frontends/lean/util): fixes #1495

We should freeze only constants
---
 src/frontends/lean/util.cpp |  2 +-
 tests/lean/run/1495.lean    | 10 ++++++++++
 2 files changed, 11 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/1495.lean

diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp
index 1b4a738377..9d6db7289a 100644
--- a/src/frontends/lean/util.cpp
+++ b/src/frontends/lean/util.cpp
@@ -418,7 +418,7 @@ bool is_frozen_name(expr const & e) {
 
 expr freeze_names(expr const & e) {
     return replace(e, [&](expr const e, unsigned) {
-            if (is_local(e) || is_constant(e))
+            if (is_constant(e))
                 return some_expr(mk_frozen_name_annotation(e));
             else
                 return none_expr();
diff --git a/tests/lean/run/1495.lean b/tests/lean/run/1495.lean
new file mode 100644
index 0000000000..15a78eba50
--- /dev/null
+++ b/tests/lean/run/1495.lean
@@ -0,0 +1,10 @@
+section
+variables (r : ℕ → ℕ → Prop)
+local infix `≼` : 50 := r
+
+example {a b : ℕ} : a ≼ b → true :=
+begin
+  show a ≼ b → true,
+    from λx, trivial
+end
+end