diff -r 7b59d2945e54 -r 1f1366966296 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Thu Mar 11 07:05:29 2021 +0000
+++ b/src/HOL/Power.thy	Thu Mar 11 07:05:38 2021 +0000
@@ -480,8 +480,9 @@
   by (induct n) auto
 
 text \<open>Surely we can strengthen this? It holds for \<open>0<a<1\<close> too.\<close>
-lemma power_inject_exp [simp]: "1 < a \<Longrightarrow> a ^ m = a ^ n \<longleftrightarrow> m = n"
-  by (force simp add: order_antisym power_le_imp_le_exp)
+lemma power_inject_exp [simp]:
+  \<open>a ^ m = a ^ n \<longleftrightarrow> m = n\<close> if \<open>1 < a\<close>
+  using that by (force simp add: order_class.order.antisym power_le_imp_le_exp)
 
 text \<open>
   Can relax the first premise to \<^term>\<open>0<a\<close> in the case of the
@@ -609,7 +610,7 @@
 qed
 
 lemma power_inject_base: "a ^ Suc n = b ^ Suc n \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a = b"
-  by (blast intro: power_le_imp_le_base antisym eq_refl sym)
+  by (blast intro: power_le_imp_le_base order.antisym eq_refl sym)
 
 lemma power_eq_imp_eq_base: "a ^ n = b ^ n \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 < n \<Longrightarrow> a = b"
   by (cases n) (simp_all del: power_Suc, rule power_inject_base)