by (CLASIMPSET auto_tac);

--- a/src/HOL/IMPP/Natural.ML	Tue Jul 25 00:13:49 2000 +0200
+++ b/src/HOL/IMPP/Natural.ML	Tue Jul 25 01:27:36 2000 +0200
@@ -38,7 +38,7 @@
 
 goal Nat.thy "(Suc n <= m') --> (? m. m' = Suc m)";
 by (induct_tac "m'" 1);
-by  Auto_tac;
+by (CLASIMPSET auto_tac);
 qed_spec_mp "Suc_le_D";
 
 Goal "[| Suc n <= m'; (!!m. n <= m ==> P (Suc m)) |] ==> P m'";