diff --git a/src/Lean/Elab/Tactic/Location.lean b/src/Lean/Elab/Tactic/Location.lean
index 6e9134d16e..6276f584ca 100644
--- a/src/Lean/Elab/Tactic/Location.lean
+++ b/src/Lean/Elab/Tactic/Location.lean
@@ -49,7 +49,7 @@ def withLocation (loc : Location) (atLocal : FVarId → TacticM Unit) (atTarget
       let fvarId ← getFVarId hyp
       atLocal fvarId
     if type then
-      atTarget
+      withMainContext atTarget
   | Location.wildcard =>
     let worked ← tryTactic <| withMainContext <| atTarget
     withMainContext do
diff --git a/tests/lean/withLocation.lean b/tests/lean/withLocation.lean
new file mode 100644
index 0000000000..a0f378575a
--- /dev/null
+++ b/tests/lean/withLocation.lean
@@ -0,0 +1,15 @@
+import Lean
+
+open Lean Elab Tactic
+elab "test" : tactic => do
+  withLocation (.targets #[] true) (fun _ => return ())
+    do
+      let some (_, lhs, _) := (← getMainTarget).eq? | failure
+      logInfo <| ← FVarId.getUserName (lhs.fvarId!)
+    (fun _ => return ())
+
+example : 1 = 1 := by
+  let t := 1
+  show t = 1
+  test
+  sorry
diff --git a/tests/lean/withLocation.lean.expected.out b/tests/lean/withLocation.lean.expected.out
new file mode 100644
index 0000000000..e6bba11d86
--- /dev/null
+++ b/tests/lean/withLocation.lean.expected.out
@@ -0,0 +1,2 @@
+t
+withLocation.lean:11:0-11:7: warning: declaration uses 'sorry'