adapted proof of less_succ: problem because of non-confluent SimpSet removed

--- a/src/FOL/ex/Nat2.ML	Thu Apr 18 12:33:05 1996 +0200
+++ b/src/FOL/ex/Nat2.ML	Thu Apr 18 14:11:02 1996 +0200
@@ -158,9 +158,7 @@
 by (IND_TAC nat_ind (simp_tac nat_ss) "j" 1);
 by (ALL_IND_TAC nat_exh (simp_tac nat_ss) 1);
 by (resolve_tac [impI RS allI] 1);
-by (rtac nat_exh 1);
-by (simp_tac nat_ss 1);
-by (simp_tac nat_ss 1);
+by (ALL_IND_TAC nat_exh (simp_tac nat_ss) 1);
 by (asm_simp_tac nat_ss 1);
 qed "less_succ";