ex/PL.ML

--- a/ex/PL.ML	Wed Aug 24 18:49:29 1994 +0200
+++ b/ex/PL.ML	Thu Aug 25 10:47:33 1994 +0200
@@ -101,8 +101,7 @@
 \     !!x. P(((x->false)->false)->x);			\
 \     !!x y. [| H |- x->y;  H |- x;  P(x->y);  P(x) |] ==> P(y) \
 \  |] ==> P(a)";
-by (rtac (major RS (thms_def RS def_induct)) 1);
-by (rtac thms_bnd_mono 1);
+by (rtac ([thms_def, thms_bnd_mono, major] MRS def_induct) 1);
 by (rewrite_tac rule_defs);
 by (fast_tac (set_cs addIs prems) 1);
 val conseq_induct = result();
@@ -267,7 +266,7 @@
 goal PL.thy "hyps(p,t) : Fin(UN v:{x.True}. {#v, #v->false})";
 by (PL.pl.induct_tac "p" 1);
 by (ALLGOALS (simp_tac (pl_ss setloop (split_tac [expand_if])) THEN'
-              fast_tac (set_cs addSIs [Fin_0I, Fin_insertI, Fin_UnI])));
+              fast_tac (set_cs addSIs Fin.intrs@[Fin_UnI])));
 val hyps_finite = result();
 
 val Diff_weaken_left = subset_refl RSN (2, Diff_mono) RS weaken_left;