# HG changeset patch
# User wenzelm
# Date 964481256 -7200
# Node ID 6f089616ae1f6dafb3ce3dc0c592dad8dc3d5a38
# Parent  e729ea747250bcdcb8f390411d4516988841be2b
by (CLASIMPSET auto_tac);

diff -r e729ea747250 -r 6f089616ae1f src/HOL/IMPP/Natural.ML
--- 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'";