--- a/src/ZF/ex/Primrec.ML Sun May 25 18:45:25 1997 +0200
+++ b/src/ZF/ex/Primrec.ML Mon May 26 12:25:15 1997 +0200
@@ -283,7 +283,7 @@
qed "COMP_map_lemma";
goalw Primrec.thy [COMP_def]
- "!!g. [| g: primrec; kg: nat; \
+ "!!g. [| kg: nat; \
\ ALL l:list(nat). g`l < ack(kg, list_add(l)); \
\ fs : list({f: primrec . \
\ EX kf:nat. ALL l:list(nat). \
@@ -319,7 +319,7 @@
assume_tac, rtac (add_le_self RS ack_lt_mono1),
REPEAT o ares_tac (ack_typechecks)] 1);
(*ind step*)
-by (asm_simp_tac (!simpset addsimps [add_succ_right]) 1);
+by (Asm_simp_tac 1);
by (rtac (succ_leI RS lt_trans1) 1);
by (res_inst_tac [("j", "g ` ?ll #+ ?mm")] lt_trans1 1);
by (etac bspec 2);