# HG changeset patch
# User paulson
# Date 958478869 -7200
# Node ID 7aec47e7d72778bc5833a1a978c28044c46894b2
# Parent  9d6514fcd584c31a46414a1414eb774a38d2ec94
changed to cope with the rewriting of #2+n to Suc(Suc n)

diff -r 9d6514fcd584 -r 7aec47e7d727 src/HOL/ex/Primrec.ML
--- 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")]