Modified proofs for new form of 'split'.

--- 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