diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp index 0ef17665a..d74385c76 100644 --- a/src/library/tactic/rewrite_tactic.cpp +++ b/src/library/tactic/rewrite_tactic.cpp @@ -743,7 +743,7 @@ class rewrite_fn { if (!oe) return none_expr(); expr new_e = *oe; - optional unfolded_e = unfold_app(m_env, new_e); + optional unfolded_e = unfold_term(m_env, new_e); if (!unfolded_e) return none_expr(); bool use_cache = occ.is_all(); diff --git a/tests/lean/run/702.lean b/tests/lean/run/702.lean new file mode 100644 index 000000000..c25b64f3e --- /dev/null +++ b/tests/lean/run/702.lean @@ -0,0 +1,6 @@ +definition bar := bool +example (b : bar) : bool := +begin + rewrite [↓bar], + assumption +end