src/HOL/Nat.thy

--- a/src/HOL/Nat.thy	Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Nat.thy	Mon Sep 12 07:55:43 2011 +0200
@@ -320,7 +320,7 @@
 
 lemma one_eq_mult_iff [simp,no_atp]: "(Suc 0 = m * n) = (m = Suc 0 & n = Suc 0)"
   apply (rule trans)
-  apply (rule_tac [2] mult_eq_1_iff, fastsimp)
+  apply (rule_tac [2] mult_eq_1_iff, fastforce)
   done
 
 lemma nat_mult_eq_1_iff [simp]: "m * n = (1::nat) \<longleftrightarrow> m = 1 \<and> n = 1"