1.1 --- a/src/HOL/Relation_Power.thy	Mon Sep 11 14:35:30 2006 +0200
     1.2 +++ b/src/HOL/Relation_Power.thy	Mon Sep 11 21:35:19 2006 +0200
     1.3 @@ -59,7 +59,7 @@
     1.4  
     1.5  lemma rel_pow_Suc_I2:
     1.6      "(x, y) : R \<Longrightarrow> (y, z) : R^n \<Longrightarrow> (x,z) : R^(Suc n)"
     1.7 -  apply (induct n fixing: z)
     1.8 +  apply (induct n arbitrary: z)
     1.9     apply simp
    1.10    apply fastsimp
    1.11    done
    1.12 @@ -79,7 +79,7 @@
    1.13  
    1.14  lemma rel_pow_Suc_D2:
    1.15      "(x, z) : R^(Suc n) \<Longrightarrow> (\<exists>y. (x,y) : R & (y,z) : R^n)"
    1.16 -  apply (induct n fixing: x z)
    1.17 +  apply (induct n arbitrary: x z)
    1.18     apply (blast intro: rel_pow_0_I elim: rel_pow_0_E rel_pow_Suc_E)
    1.19    apply (blast intro: rel_pow_Suc_I elim: rel_pow_0_E rel_pow_Suc_E)
    1.20    done