diff --git a/Game/MyNat/Power.lean b/Game/MyNat/Power.lean
index 6da80a7..1031fc0 100644
--- a/Game/MyNat/Power.lean
+++ b/Game/MyNat/Power.lean
@@ -10,7 +10,7 @@ instance : Pow ℕ ℕ where
   pow := pow
 
 -- Note: since v4.2.0-rc2
-macro_rules | `($x ^ $y)   => `(Pow.pow $x ($y : MyNat))
+macro_rules | `($x ^ $y)   => `(HPow.hPow ($x : MyNat) ($y : MyNat))
 
 @[MyNat_decide]
 axiom pow_zero (m : ℕ) : m ^ 0 = 1