Used 2 instead of Suc(Suc 0)

--- a/src/HOL/ex/NatSum.ML	Mon Jun 03 11:41:00 1996 +0200
+++ b/src/HOL/ex/NatSum.ML	Mon Jun 03 11:41:26 1996 +0200
@@ -9,7 +9,7 @@
 Addsimps ([NatSum.sum_0,NatSum.sum_Suc] @ add_ac);
 
 (*The sum of the first n positive integers equals n(n+1)/2.*)
-goal NatSum.thy "Suc(Suc(0))*sum (%i.i) (Suc n) = n*Suc(n)";
+goal NatSum.thy "2*sum (%i.i) (Suc n) = n*Suc(n)";
 by (Simp_tac 1);
 by (nat_ind_tac "n" 1);
 by (Simp_tac 1);