Disable certain notation

Stream: lean4

[Horațiu Cheval]

Is there a way to disable a certain notation? After updating to 11-10 my code depending on Mathlib 4 no longer works

import Mathlib

inductive Foo where
| implication : Foo → Foo → Foo

infixr:60 " ⇒ " => Foo.implication

def Foo.bar : Foo → Int
| x ⇒ y => x.bar + y.bar

probably because ⇒ was introduced as a notation for Relator.LiftFun. The notation works normally, only in pattern matching it fails with
invalid pattern, constructor or constant marked with '[match_pattern]' expected. Can I somehow hide this notation when importing Mathlib or is changing my notation the only fix?

[Mario Carneiro]

you can use (priority := high) on your syntax, I think

[Horațiu Cheval]

Thanks! That fixed it

[Mario Carneiro]

(that relator notation should be scoped though)