diff --git a/src/frontends/lean/tactic_notation.cpp b/src/frontends/lean/tactic_notation.cpp
index f7f8fda0c1..e7bf31284d 100644
--- a/src/frontends/lean/tactic_notation.cpp
+++ b/src/frontends/lean/tactic_notation.cpp
@@ -274,8 +274,8 @@ struct parse_tactic_fn {
             auto pos = m_p.pos();
             name const & end_tk = m_p.curr_is_token(get_begin_tk()) ? get_end_tk() : get_rcurly_tk();
             expr next_tac = parse_block(pos, end_tk);
-            // auto block_pos = m_p.pos_of(next_tac);
-            next_tac       = mk_tactic_solve1(m_p, next_tac, pos, m_tac_class, m_use_istep && save_info);
+            auto end_pos = m_p.pos_of(next_tac);
+            next_tac       = mk_tactic_solve1(m_p, next_tac, end_pos, m_tac_class, m_use_istep && save_info);
             if (save_info) {
                 expr info_tac = mk_tactic_save_info(m_p, pos, m_tac_class);
                 return concat(info_tac, next_tac, pos);
diff --git a/tests/lean/auto_quote_error2.lean b/tests/lean/auto_quote_error2.lean
index ad615ed2bf..1e9cd714ea 100644
--- a/tests/lean/auto_quote_error2.lean
+++ b/tests/lean/auto_quote_error2.lean
@@ -37,3 +37,11 @@ begin
     exact eq.trans h1 _, -- Error unsolved
   end,
 end
+
+example (a b : nat) : a = 0 → b = 0 → a = b ∧ b = a :=
+begin
+   intros h1 h2,
+   split,
+   { subst h1 },
+            --^ error should be at `}`
+end
diff --git a/tests/lean/auto_quote_error2.lean.expected.out b/tests/lean/auto_quote_error2.lean.expected.out
index 7399980631..c10c1cafaf 100644
--- a/tests/lean/auto_quote_error2.lean.expected.out
+++ b/tests/lean/auto_quote_error2.lean.expected.out
@@ -13,20 +13,20 @@ a_1 : a = b,
 a_2 : b = c
 ⊢ Sort ?
 hello world
-auto_quote_error2.lean:14:2: error: focus tactic failed, focused goal has not been solved
+auto_quote_error2.lean:16:2: error: focus tactic failed, focused goal has not been solved
 state:
 a b c : ℕ,
 a_1 : a = b,
 a_2 : b = c
 ⊢ a = c
 hello world
-auto_quote_error2.lean:26:2: error: focus tactic failed, focused goal has not been solved
+auto_quote_error2.lean:28:2: error: focus tactic failed, focused goal has not been solved
 state:
 a b c : ℕ,
 a_1 : a = b,
 a_2 : b = c
 ⊢ a = ?m_1
-auto_quote_error2.lean:37:22: error: don't know how to synthesize placeholder
+auto_quote_error2.lean:38:2: error: don't know how to synthesize placeholder
 context:
 a b c : ℕ,
 h1 : a = b,
@@ -37,3 +37,8 @@ a b c : ℕ,
 h1 : a = b,
 h2 : b = c
 ⊢ a = c
+auto_quote_error2.lean:45:14: error: focus tactic failed, focused goal has not been solved
+state:
+b : ℕ,
+h2 : b = 0
+⊢ 0 = b