diff --git a/Std/Tactic/SqueezeScope.lean b/Std/Tactic/SqueezeScope.lean
index 820618d84a..de1ed24aae 100644
--- a/Std/Tactic/SqueezeScope.lean
+++ b/Std/Tactic/SqueezeScope.lean
@@ -107,8 +107,9 @@ elab_rules : tactic
       | some mvarId => replaceMainGoal [mvarId]
       pure usedSimps
     | ``Parser.Tactic.dsimp => do
-      let { ctx, .. } ← withMainContext <| mkSimpContext stx (eraseLocal := false) (kind := .dsimp)
-      dsimpLocation' ctx (expandOptLocation stx[5])
+      let { ctx, simprocs, .. } ←
+        withMainContext <| mkSimpContext stx (eraseLocal := false) (kind := .dsimp)
+      dsimpLocation' ctx simprocs (expandOptLocation stx[5])
     | _ => Elab.throwUnsupportedSyntax
     let a := a.getId; let x := x.getId
     squeezeScopes.modify fun map => Id.run do