Binding the syntax being matched in `elab_rules`?

Stream: lean4

[Scott Morrison]

I want to change a use of

elab tk:"librarySearch" : tactic => do

to

elab_rules : tactic | `(librarySearch) => do ...

(as there will now be a syntax declaration earlier).

However I do still need the tk : Syntax later in the tactic, and I'm not sure how to obtain it when using elab_rules. How can I do this?

[Scott Morrison]

Specifically I want to make the change here.

[Mac]

@Scott Morrison You can do get tk like so:

elab_rules : tactic | `(librarySearch%$tk) => do ...