src/ZF/Nat.thy

     "[| m: nat;  n: nat;   
         !!x. x: nat ==> P(x,0);   
         !!y. y: nat ==> P(0,succ(y));   
         !!x y. [| x: nat;  y: nat;  P(x,y) |] ==> P(succ(x),succ(y)) |]
      ==> P(m,n)"
-apply (erule_tac x = "m" in rev_bspec)
+apply (erule_tac x = m in rev_bspec)
 apply (erule nat_induct, simp) 
 apply (rule ballI)
 apply (rename_tac i j)
 apply (erule_tac n=j in nat_induct, auto)  
 done