Local instances not captured correctly in term sorries

I came across a new bug: local instances are not captured correctly in term sorries for the tactic mode.

Example input:

{"cmd": "def test (α : Type) [s : Inhabited α] : α := @Inhabited.default α s"}

{"cmd": "def test2 (α : Type) [Inhabited α] : α := by exact test α", "env": 0}

{"cmd": "def test2 (α : Type) [Inhabited α] : α := sorry", "env": 0}

{"tactic": "exact test α", "proofState": 0}

Output:

{"env": 0}

{"env": 1}

{"sorries":
 [{"proofState": 0,
   "pos": {"line": 1, "column": 42},
   "goal": "α : Type\ninst✝ : Inhabited α\n⊢ α",
   "endPos": {"line": 1, "column": 47}}],
 "messages":
 [{"severity": "warning",
   "pos": {"line": 1, "column": 4},
   "endPos": {"line": 1, "column": 9},
   "data": "declaration uses 'sorry'"}],
 "env": 2}


{"proofStatus": "Incomplete: contains sorry",
 "proofState": 1,
 "messages":
 [{"severity": "error",
   "pos": {"line": 0, "column": 0},
   "endPos": {"line": 0, "column": 0},
   "data":
   "failed to synthesize\n  Inhabited α\n\nAdditional diagnostic information may be available using the `set_option diagnostics true` command."}],
 "goals": []}

Reproduce the JSON command sequence and tactic request shown in the issue, then trace how tactic-mode term sorries collect local instances. Done means the final exact test α request succeeds with the local Inhabited α instance captured correctly, without the reported synthesis error.