diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index a35ef53973..0e8b16880d 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -253,8 +253,12 @@ private meta def is_neg (p : pexpr) : option pexpr :=
 /- Remark: we use the low-level to_raw_expr and of_raw_expr to be able to
    pattern match pre-terms. This is a low-level trick (aka hack). -/
 match pexpr.to_raw_expr p with
-| (app (const c []) arg) := if c = `neg then some (pexpr.of_raw_expr arg) else none
-| _                      := none
+| (app fn arg) :=
+  match fn^.erase_annotations with
+  | (const `neg _) := some (pexpr.of_raw_expr arg)
+  | _              := none
+  end
+| _            := none
 end
 
 private meta def resolve_name' (n : name) : tactic expr :=
diff --git a/src/frontends/lean/calc.cpp b/src/frontends/lean/calc.cpp
index 90bfbc196f..2a100f1778 100644
--- a/src/frontends/lean/calc.cpp
+++ b/src/frontends/lean/calc.cpp
@@ -55,7 +55,7 @@ static calc_pred decode_expr(expr const & e, pos_info const & pos) {
         throw parser_error("invalid 'calc' expression, overloaded expressions are not supported", pos);
     } else {
         buffer<expr> args;
-        expr const & fn = get_app_args(e, args);
+        expr const & fn = get_nested_annotation_arg(get_app_args(e, args));
         unsigned nargs  = args.size();
         if (!is_constant(fn) || nargs < 2) {
             throw parser_error("invalid 'calc' expression, expression must be a function application 'f a_1 ... a_k' "
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 3ac30f44e1..ac2936b644 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -2808,6 +2808,8 @@ expr elaborator::visit_macro(expr const & e, optional<expr> const & expected_typ
         return mk_sorry(expected_type, e);
     } else if (is_structure_instance(e)) {
         return visit_structure_instance(e, expected_type);
+    } else if (is_frozen_name(e)) {
+        return visit(get_annotation_arg(e), expected_type);
     } else if (is_annotation(e)) {
         expr r = visit(get_annotation_arg(e), expected_type);
         return update_macro(e, 1, &r);
@@ -3706,6 +3708,8 @@ struct resolve_names_fn : public replace_visitor {
             return e;
         } else if (is_choice(e)) {
             return visit_choice(e);
+        } else if (is_frozen_name(e)) {
+            return get_annotation_arg(e);
         } else {
             return replace_visitor::visit(e);
         }
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 2a222ac00f..adee741849 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -1438,7 +1438,10 @@ expr parser::parse_notation(parse_table t, expr * left) {
         }
     }
     for (notation::accepting const & a : as) {
-        expr r = copy_with_new_pos(a.get_expr(), p);
+        expr a_expr = a.get_expr();
+        if (m_in_quote)
+            a_expr = freeze_names(a_expr);
+        expr r = copy_with_new_pos(a_expr, p);
         list<notation::action> const & postponed = a.get_postponed();
         if (postponed) {
             buffer<expr> new_args;
diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp
index d366c51887..d9d7b568ce 100644
--- a/src/frontends/lean/util.cpp
+++ b/src/frontends/lean/util.cpp
@@ -392,12 +392,34 @@ expr parse_auto_param(parser & p, expr const & type) {
     return mk_auto_param(type, const_name(tac_expr));
 }
 
+static name * g_frozen_name = nullptr;
+
+expr mk_frozen_name_annotation(expr const & e) {
+    return mk_annotation(*g_frozen_name, e);
+}
+
+bool is_frozen_name(expr const & e) {
+    return is_annotation(e, *g_frozen_name);
+}
+
+expr freeze_names(expr const & e) {
+    return replace(e, [&](expr const e, unsigned) {
+            if (is_local(e) || is_constant(e))
+                return some_expr(mk_frozen_name_annotation(e));
+            else
+                return none_expr();
+        });
+}
+
 void initialize_frontend_lean_util() {
     g_no_info = new name("no_info");
     register_annotation(*g_no_info);
+    g_frozen_name = new name("frozen_name");
+    register_annotation(*g_frozen_name);
 }
 
 void finalize_frontend_lean_util() {
     delete g_no_info;
+    delete g_frozen_name;
 }
 }
diff --git a/src/frontends/lean/util.h b/src/frontends/lean/util.h
index 34131b7bbf..9300d84a5e 100644
--- a/src/frontends/lean/util.h
+++ b/src/frontends/lean/util.h
@@ -117,6 +117,17 @@ expr mk_opt_param(expr const & t, expr const & val);
 expr mk_auto_param(expr const & t, name const & tac_name);
 expr parse_auto_param(parser & p, expr const & type);
 
+/* Add frozen annotation around constants and local constants occurring in \c e.
+   This annotation is used to prevent lean from resolving the names again
+   at tactic execution time. See resolve_names_fn at elaborator.cpp.
+
+   In notation declarations, names are resolved at notation declaration time.
+   Users do not expect them to be resolved again at tactic execution time.
+   See issue #1468. */
+expr freeze_names(expr const & e);
+/* Return true iff \c e is marked with a frozen_name annotation. */
+bool is_frozen_name(expr const & e);
+
 void initialize_frontend_lean_util();
 void finalize_frontend_lean_util();
 }
diff --git a/tests/lean/run/1468.lean b/tests/lean/run/1468.lean
new file mode 100644
index 0000000000..a824a40cb1
--- /dev/null
+++ b/tests/lean/run/1468.lean
@@ -0,0 +1,17 @@
+local infix * := _root_.mul
+
+namespace Y
+def mul : bool → bool := λ b, b
+
+example (m n : ℕ) : true :=
+begin
+definev k : ℕ := m * n,
+definev a : bool := mul tt,
+trivial
+end
+end Y
+
+
+meta def is_mul : expr → option (expr × expr)
+| ```(%%a * %%b) := some (a, b)
+| _              := none