diff --git a/src/frontends/lean/parse_rewrite_tactic.cpp b/src/frontends/lean/parse_rewrite_tactic.cpp index 126a6ce26..7888143b7 100644 --- a/src/frontends/lean/parse_rewrite_tactic.cpp +++ b/src/frontends/lean/parse_rewrite_tactic.cpp @@ -35,7 +35,7 @@ static expr parse_rule(parser & p) { expr parse_rewrite_element(parser & p) { if (p.curr_is_token(get_up_tk()) || p.curr_is_token(get_caret_tk())) { p.next(); - name n = p.check_id_next("invalid unfold rewrite step, identifier expected"); + name n = p.check_constant_next("invalid unfold rewrite step, constant expected"); location loc = parse_tactic_location(p); return mk_rewrite_unfold(n, loc); }