src/ZF/Cardinal.ML

--- a/src/ZF/Cardinal.ML	Wed May 22 17:25:40 2002 +0200
+++ b/src/ZF/Cardinal.ML	Wed May 22 17:26:34 2002 +0200
@@ -472,7 +472,7 @@
 qed "succ_lepoll_succD";
 
 Goal "m:nat ==> ALL n: nat. m lepoll n --> m le n";
-by (nat_ind_tac "m" [] 1);  (*induct_tac isn't available yet*)
+by (etac nat_induct 1);  (*induct_tac isn't available yet*)
 by (blast_tac (claset() addSIs [nat_0_le]) 1);
 by (rtac ballI 1);
 by (eres_inst_tac [("n","n")] natE 1);