# HG changeset patch
# User paulson
# Date 864642315 -7200
# Node ID 480ad4e726623dec49a8697d41ea3fa2565f1ffc
# Parent  9b8e638f8602f0fb86fa7102072edf15f5bdfd94
Slight simplifications

diff -r 9b8e638f8602 -r 480ad4e72662 src/ZF/ex/Primrec.ML
--- 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);