src/ZF/Nat.thy

--- a/src/ZF/Nat.thy	Thu Jan 23 09:16:53 2003 +0100
+++ b/src/ZF/Nat.thy	Thu Jan 23 10:30:14 2003 +0100
@@ -174,7 +174,7 @@
         !!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)