# HG changeset patch
# User haftmann
# Date 1235137763 -3600
# Node ID cc264a9a033dbefd118935f3e075453bf2fff93f
# Parent  862fc7751a1582ec92be65a4ecdbf663145fd0b3
consider changes variable names in theorem le_imp_power_dvd

diff -r 862fc7751a15 -r cc264a9a033d src/HOL/Algebra/Exponent.thy
--- a/src/HOL/Algebra/Exponent.thy	Fri Feb 20 10:14:32 2009 +0100
+++ b/src/HOL/Algebra/Exponent.thy	Fri Feb 20 14:49:23 2009 +0100
@@ -210,7 +210,7 @@
 
 lemma p_fac_forw: "[| (m::nat) > 0; k>0; k < p^a; (p^r) dvd (p^a)* m - k |]  
   ==> (p^r) dvd (p^a) - k"
-apply (frule_tac k1 = k and i = p in p_fac_forw_lemma [THEN le_imp_power_dvd], auto)
+apply (frule p_fac_forw_lemma [THEN le_imp_power_dvd, of _ k p], auto)
 apply (subgoal_tac "p^r dvd p^a*m")
  prefer 2 apply (blast intro: dvd_mult2)
 apply (drule dvd_diffD1)
@@ -226,7 +226,7 @@
 
 lemma p_fac_backw: "[| m>0; k>0; (p::nat)\<noteq>0;  k < p^a;  (p^r) dvd p^a - k |]  
   ==> (p^r) dvd (p^a)*m - k"
-apply (frule_tac k1 = k and i = p in r_le_a_forw [THEN le_imp_power_dvd], auto)
+apply (frule_tac k1 = k and p1 = p in r_le_a_forw [THEN le_imp_power_dvd], auto)
 apply (subgoal_tac "p^r dvd p^a*m")
  prefer 2 apply (blast intro: dvd_mult2)
 apply (drule dvd_diffD1)