diff --git a/src/library/tactic/location.cpp b/src/library/tactic/location.cpp
index 8dfd0a0ee..aa3b615bd 100644
--- a/src/library/tactic/location.cpp
+++ b/src/library/tactic/location.cpp
@@ -113,6 +113,7 @@ deserializer & operator>>(deserializer & d, location & loc) {
 }
 
 expr replace_occurrences(expr const & e, expr const & t, occurrence const & occ, unsigned idx) {
+    bool use_cache   = occ.is_all();
     unsigned occ_idx = 0;
     return replace(e, [&](expr const & e, unsigned offset) {
             if (e == t) {
@@ -121,6 +122,6 @@ expr replace_occurrences(expr const & e, expr const & t, occurrence const & occ,
                     return some_expr(mk_var(offset+idx));
             }
             return none_expr();
-        });
+        }, use_cache);
 }
 }
diff --git a/tests/lean/run/rewrite5.lean b/tests/lean/run/rewrite5.lean
new file mode 100644
index 000000000..826274e78
--- /dev/null
+++ b/tests/lean/run/rewrite5.lean
@@ -0,0 +1,9 @@
+import algebra.group
+open algebra
+
+variable {A : Type}
+variable [s : group A]
+include s
+
+theorem mul.right_inv (a : A) : a * a⁻¹ = 1 :=
+by rewrite ⟨-{a}inv_inv at {1}, mul.left_inv⟩