diff --git a/Tactics/Sym.lean b/Tactics/Sym.lean
index 5a62f834..b0d5621f 100644
--- a/Tactics/Sym.lean
+++ b/Tactics/Sym.lean
@@ -244,7 +244,7 @@ elab "explode_step" h_step:term " at " state:term : tactic => withMainContext do
   let .fvar stateFVar := state
     | throwError "Expected fvar, found {state}"
   let stateDecl := (← getLCtx).get! stateFVar
-  let c ← SymContext.fromLocalContext (some stateDecl.userName)
+  let c ← SymContext.fromMainContext (some stateDecl.userName)
   let _ ← SymM.run c <| explodeStep hStep
 
 /--
@@ -403,11 +403,8 @@ elab "sym_n" whileTac?:(sym_while)? n:num s:(sym_at)? : tactic => do
         omega;
         ))
 
-  let c ← withMainContext <| SymContext.fromLocalContext s
-  SymM.run' c <| do
-    -- Context preparation
-    canonicalizeHypothesisTypes
-
+  let c ← SymContext.fromMainContext s
+  SymM.run' c <| withMainContext' <|  do
     -- Check pre-conditions
     assertStepTheoremsGenerated
     let n ← ensureAtMostRunSteps n.getNat
diff --git a/Tactics/Sym/Context.lean b/Tactics/Sym/Context.lean
index 6d729d26..1afc1f73 100644
--- a/Tactics/Sym/Context.lean
+++ b/Tactics/Sym/Context.lean
@@ -415,14 +415,15 @@ protected def searchFor : SearchLCtxForM SymM Unit := do
 
   return ()
 
-/-- Build a `SymContext` by searching the local context for hypotheses of the
-required types (up-to defeq) . The local context is modified to unfold the types
-to be syntactically equal to the expected type.
+/-- Build a `SymContext` by searching the local context of the main goal for
+hypotheses of the required types (up-to defeq).
+The local context is modified to unfold the types to be syntactically equal to
+the expected types.
 
 If an hypothesis `h_err : r <state> .ERR = None` is not found,
-we create a new subgoal of this type
+we create a new subgoal of this type.
 -/
-def fromLocalContext (state? : Option Name) : TacticM SymContext := do
+def fromMainContext (state? : Option Name) : TacticM SymContext := do
   let msg := m!"Building a `SymContext` from the local context"
   withTraceNode `Tactic.sym (fun _ => pure msg) <| withMainContext' do
   trace[Tactic.Sym] "state? := {state?}"