diff --git a/MIL/C12_Integration_and_Measure_Theory/S01_Elementary_Integration.lean b/MIL/C12_Integration_and_Measure_Theory/S01_Elementary_Integration.lean
index cb7f5171..034134d2 100644
--- a/MIL/C12_Integration_and_Measure_Theory/S01_Elementary_Integration.lean
+++ b/MIL/C12_Integration_and_Measure_Theory/S01_Elementary_Integration.lean
@@ -3,8 +3,6 @@ import Mathlib.MeasureTheory.Integral.IntervalIntegral
 import Mathlib.Analysis.SpecialFunctions.Integrals
 import Mathlib.Analysis.Convolution
 
-local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y)
-
 open Set Filter
 
 open Topology Filter