src/HOL/Nat.thy

--- a/src/HOL/Nat.thy	Tue Oct 23 12:47:21 2007 +0200
+++ b/src/HOL/Nat.thy	Tue Oct 23 13:10:19 2007 +0200
@@ -1104,8 +1104,8 @@
   apply (drule sym)
   apply (rule disjCI)
   apply (rule nat_less_cases, erule_tac [2] _)
-  apply (fastsimp elim!: less_SucE)
-  apply (auto simp add: neq0_conv dest: mult_less_mono2)
+   apply (drule_tac [2] mult_less_mono2)
+    apply (auto simp add: neq0_conv)
   done