# 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(<a,<b,c>>,%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