From 0fc2efe88e5f08aef081319ef8a1c8b2e78b07b3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 28 Jun 2015 20:37:17 -0700
Subject: [PATCH] fix(library/tactic/rewrite_tactic): fixes #702

---
 src/library/tactic/rewrite_tactic.cpp | 2 +-
 tests/lean/run/702.lean               | 6 ++++++
 2 files changed, 7 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/702.lean

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<expr> unfolded_e = unfold_app(m_env, new_e);
+        optional<expr> 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