diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean
index aaff02d..43f3e85 100644
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@@ -74,13 +74,14 @@ protected def GoalState.metaState (state: GoalState): Meta.State :=
 protected def GoalState.coreState (state: GoalState): Core.SavedState :=
   state.savedState.term.meta.core
 
-protected def GoalState.withContext (state: GoalState) (mvarId: MVarId) (m: MetaM α): MetaM α := do
+protected def GoalState.withContext' (state: GoalState) (mvarId: MVarId) (m: MetaM α): MetaM α := do
   mvarId.withContext m |>.run' (← read) state.metaState
-
+protected def GoalState.withContext { m } [MonadControlT MetaM m] [Monad m] (state: GoalState) (mvarId: MVarId) : m α → m α :=
+  Meta.mapMetaM <| state.withContext' mvarId
 protected def GoalState.withParentContext { n } [MonadControlT MetaM n] [Monad n] (state: GoalState): n α → n α :=
-  Meta.mapMetaM <| state.withContext state.parentMVar?.get!
+  Meta.mapMetaM <| state.withContext' state.parentMVar?.get!
 protected def GoalState.withRootContext { n } [MonadControlT MetaM n] [Monad n] (state: GoalState): n α → n α :=
-  Meta.mapMetaM <| state.withContext state.root
+  Meta.mapMetaM <| state.withContext' state.root
 
 private def GoalState.mvars (state: GoalState): SSet MVarId :=
   state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k