changed to cope with the rewriting of #2+n to Suc(Suc n)

--- a/src/HOL/ex/Primrec.ML	Tue May 16 14:07:06 2000 +0200
+++ b/src/HOL/ex/Primrec.ML	Tue May 16 14:07:49 2000 +0200
@@ -150,7 +150,7 @@
 by (res_inst_tac [("j", "ack(2, ack(i1 + i2, j))")] less_trans 1);
 by (Asm_simp_tac 1);
 by (rtac (ack_nest_bound RS less_le_trans) 2);
-by (Asm_simp_tac 2);
+by (asm_simp_tac (simpset() addsimps [Suc3_eq_add_3]) 2);
 by (cut_inst_tac [("i","i1"), ("m1","i2"), ("k","j")] 
     (le_add1 RS ack_le_mono1) 1);
 by (cut_inst_tac [("i","i2"), ("m1","i1"), ("k","j")]