diff -r 6ddb43c6b711 -r 2accfb71e33b src/HOL/Algebra/Exponent.thy
--- a/src/HOL/Algebra/Exponent.thy	Mon Aug 08 14:13:14 2016 +0200
+++ b/src/HOL/Algebra/Exponent.thy	Mon Aug 08 17:47:51 2016 +0200
@@ -15,8 +15,8 @@
 
 text\<open>needed in this form to prove Sylow's theorem\<close>
 corollary (in algebraic_semidom) div_combine: 
-  "\<lbrakk>is_prime_elem p; \<not> p ^ Suc r dvd n; p ^ (a + r) dvd n * k\<rbrakk> \<Longrightarrow> p ^ a dvd k"
-  by (metis add_Suc_right mult.commute prime_power_dvd_cases)
+  "\<lbrakk>prime_elem p; \<not> p ^ Suc r dvd n; p ^ (a + r) dvd n * k\<rbrakk> \<Longrightarrow> p ^ a dvd k"
+  by (metis add_Suc_right mult.commute prime_elem_power_dvd_cases)
 
 lemma exponent_p_a_m_k_equation: 
   fixes p :: nat
@@ -61,16 +61,16 @@
   case (Suc k)
   then have *: "(Suc (j+k) choose Suc k) > 0" by simp
   then have "multiplicity p ((Suc (j+k) choose Suc k) * Suc k) = multiplicity p (Suc k)"
-    by (subst Suc_times_binomial_eq [symmetric], subst prime_multiplicity_mult_distrib)
+    by (subst Suc_times_binomial_eq [symmetric], subst prime_elem_multiplicity_mult_distrib)
        (insert p Suc.prems, simp_all add: eeq [symmetric] Suc.IH)
   with p * show ?case
-    by (subst (asm) prime_multiplicity_mult_distrib) simp_all
+    by (subst (asm) prime_elem_multiplicity_mult_distrib) simp_all
 qed
 
 text\<open>The lemma above, with two changes of variables\<close>
 lemma p_not_div_choose:
   assumes "k < K" and "k \<le> n" 
-      and eeq: "\<And>j. \<lbrakk>0<j; j<K\<rbrakk> \<Longrightarrow> multiplicity p (n - k + (K - j)) = multiplicity p (K - j)" "is_prime p"
+      and eeq: "\<And>j. \<lbrakk>0<j; j<K\<rbrakk> \<Longrightarrow> multiplicity p (n - k + (K - j)) = multiplicity p (K - j)" "prime p"
     shows "multiplicity p (n choose k) = 0"
 apply (rule p_not_div_choose_lemma [of K p "n-k" k, simplified assms nat_minus_add_max max_absorb1])
 apply (metis add_Suc_right eeq diff_diff_cancel order_less_imp_le zero_less_Suc zero_less_diff)
@@ -78,7 +78,7 @@
 done
 
 proposition const_p_fac:
-  assumes "m>0" and prime: "is_prime p"
+  assumes "m>0" and prime: "prime p"
   shows "multiplicity p (p^a * m choose p^a) = multiplicity p m"
 proof-
   from assms have p: "0 < p ^ a" "0 < p^a * m" "p^a \<le> p^a * m"
@@ -93,13 +93,13 @@
       by (subst times_binomial_minus1_eq [symmetric]) (auto simp: prime_gt_0_nat)
     also from p have "p ^ a - Suc 0 \<le> p ^ a * m - Suc 0" by linarith
     with prime * p have "multiplicity p ?rhs = multiplicity p (p ^ a * m)"
-      by (subst prime_multiplicity_mult_distrib) auto
+      by (subst prime_elem_multiplicity_mult_distrib) auto
     also have "\<dots> = a + multiplicity p m" 
-      using prime p by (subst prime_multiplicity_mult_distrib) simp_all
+      using prime p by (subst prime_elem_multiplicity_mult_distrib) simp_all
     finally show ?thesis .
   qed
   then show ?thesis
-    using prime p by (subst (asm) prime_multiplicity_mult_distrib) simp_all
+    using prime p by (subst (asm) prime_elem_multiplicity_mult_distrib) simp_all
 qed
 
 end