diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index 9add88f68e..5699c7ff14 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -36,7 +36,6 @@ def Term.reportUnsolvedGoals (goals : List MVarId) : TermElabM Unit :=
 namespace Tactic
 
 structure Context where
-  main       : MVarId
   /-- Declaration name of the executing elaborator, used by `mkTacticInfo` to persist it in the info tree -/
   elaborator : Name
   /--
@@ -94,7 +93,7 @@ def run (mvarId : MVarId) (x : TacticM Unit) : TermElabM (List MVarId) :=
        else
          throw ex
    try
-     aux.runCore' { main := mvarId, elaborator := Name.anonymous } { goals := [mvarId] }
+     aux.runCore' { elaborator := Name.anonymous } { goals := [mvarId] }
    finally
      modify fun s => { s with syntheticMVars := savedSyntheticMVars }