Modified proof to work with miniscoping

--- a/src/FOL/ex/Nat2.ML	Thu Sep 05 18:42:48 1996 +0200
+++ b/src/FOL/ex/Nat2.ML	Fri Sep 06 10:45:48 1996 +0200
@@ -134,6 +134,7 @@
 by (simp_tac nat_ss 1);
 by (resolve_tac [impI RS allI] 1);
 by (ALL_IND_TAC nat_exh (simp_tac nat_ss) 1);
+by (resolve_tac [impI] 1);
 by (ALL_IND_TAC nat_exh (simp_tac nat_ss) 1);
 by (fast_tac FOL_cs 1);
 qed "le_trans";