diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 672c106c5..0797e2f56 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -849,6 +849,7 @@ static environment override_cmd(parser & p) { ns = *real_ns; bool persistent = false; env = override_notation(env, ns, persistent); + env = overwrite_aliases(env, ns, name()); env = update_fingerprint(env, ns.hash()); } return env; diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 723e2c7aa..5c1fcb78a 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -564,6 +564,7 @@ static expr parse_override_notation(parser & p, unsigned, expr const *, pos_info name n = p.check_id_next("invalid '#' local notation, identifier expected"); bool persistent = false; environment env = override_notation(p.env(), n, persistent); + env = overwrite_aliases(env, n, name()); return p.parse_expr_with_env(env); }