--- a/src/ZF/Sum.ML Thu May 04 02:00:38 1995 +0200
+++ b/src/ZF/Sum.ML Thu May 04 02:01:24 1995 +0200
@@ -119,13 +119,11 @@
(*** Eliminator -- case ***)
goalw Sum.thy sum_defs "case(c, d, Inl(a)) = c(a)";
-by (rtac (split RS trans) 1);
-by (rtac cond_0 1);
+by (simp_tac (ZF_ss addsimps [cond_0]) 1);
qed "case_Inl";
goalw Sum.thy sum_defs "case(c, d, Inr(b)) = d(b)";
-by (rtac (split RS trans) 1);
-by (rtac cond_1 1);
+by (simp_tac (ZF_ss addsimps [cond_1]) 1);
qed "case_Inr";
val major::prems = goal Sum.thy