--- a/src/HOL/Power.thy Sun Jan 19 14:50:03 2020 +0100
+++ b/src/HOL/Power.thy Tue Jan 21 11:02:27 2020 +0100
@@ -377,7 +377,7 @@
end
-context normalization_semidom
+context normalization_semidom_multiplicative
begin
lemma normalize_power: "normalize (a ^ n) = normalize a ^ n"