chore: work around grind bootstrap issue

src/Lean/Elab/Tactic/Grind.lean

@@ -56,14 +56,14 @@ private def elabFallback (fallback? : Option Term) : TermElabM (Grind.GoalM Unit
     pure auxDeclName
   unsafe evalConst (Grind.GoalM Unit) auxDeclName
 
-@[builtin_tactic Lean.Parser.Tactic.grind] def evalApplyRfl : Tactic := fun stx => do
-  match stx with
-  | `(tactic| grind $config:optConfig $[on_failure $fallback?]?) =>
-    let fallback ← elabFallback fallback?
-    logWarningAt stx "The `grind` tactic is experimental and still under development. Avoid using it in production projects"
-    let declName := (← Term.getDeclName?).getD `_grind
-    let config ← elabGrindConfig config
-    withMainContext do liftMetaFinishingTactic (grind · config declName fallback)
-  | _ => throwUnsupportedSyntax
+@[builtin_tactic Lean.Parser.Tactic.grind] def evalGrind : Tactic := fun stx => do
+  -- grind $config:optConfig $[on_failure $fallback?]?
+  let config := stx[1]
+  let fallback? := guard (stx[2].getNumArgs == 2) *> pure (TSyntax.mk stx[2][1])
+  let fallback ← elabFallback fallback?
+  logWarningAt stx "The `grind` tactic is experimental and still under development. Avoid using it in production projects"
+  let declName := (← Term.getDeclName?).getD `_grind
+  let config ← elabGrindConfig config
+  withMainContext do liftMetaFinishingTactic (grind · config declName fallback)
 
 end Lean.Elab.Tactic