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