# HG changeset patch # User lcp # Date 748602979 -7200 # Node ID e37080f41102a361f308600045ea7b11f1d468d9 # Parent c1795fac88c3c15380682e70bb83743f1c1ce586 This commit should not have been necessary. For some reason, the previous commit did not update genrec.ML. There were still occurrences of SIMP_TAC. Was the commit perhaps interrupted?? diff -r c1795fac88c3 -r e37080f41102 src/CCL/genrec.ML --- a/src/CCL/genrec.ML Mon Sep 20 18:39:45 1993 +0200 +++ b/src/CCL/genrec.ML Tue Sep 21 11:16:19 1993 +0200 @@ -43,7 +43,7 @@ val letrec2T = result(); goal Wfd.thy "SPLIT(>,%x xs.SPLIT(xs,%y z.B(x,y,z))) = B(a,b,c)"; -by (SIMP_TAC (ccl_ss addrews [SPLITB]) 1); +by (simp_tac (ccl_ss addsimps [SPLITB]) 1); val lemma = result(); val prems = goalw Wfd.thy [letrec3_def] @@ -55,7 +55,7 @@ \ letrec g x y z be h(x,y,z,g) in g(a,b,c) : D(a,b,c)"; br (lemma RS subst) 1; by (REPEAT (ares_tac ([letrecT,pairT,splitT]@prems) 1)); -by (SIMP_TAC (ccl_ss addrews [SPLITB]) 1); +by (simp_tac (ccl_ss addsimps [SPLITB]) 1); by (REPEAT (ares_tac ([ballI,SubtypeI]@prems) 1)); br (lemma RS subst) 1; by (REPEAT (ares_tac ([letrecT,SubtypeI,pairT,splitT]@prems) 1 ORELSE