src/HOL/Old_Number_Theory/WilsonRuss.thy

--- a/src/HOL/Old_Number_Theory/WilsonRuss.thy	Thu Nov 12 11:22:26 2015 +0100
+++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy	Fri Nov 13 12:27:13 2015 +0000
@@ -133,7 +133,7 @@
     5 \<le> p \<Longrightarrow> 0 < a \<Longrightarrow> a < p ==> inv p (inv p a) = a"
   apply (unfold inv_def)
   apply (subst power_mod)
-  apply (subst zpower_zpower)
+  apply (subst power_mult [symmetric])
   apply (rule zcong_zless_imp_eq)
       prefer 5
       apply (subst zcong_zmod)