--- a/src/HOL/Sum.ML Mon Jul 26 16:32:23 1999 +0200
+++ b/src/HOL/Sum.ML Tue Jul 27 10:29:46 1999 +0200
@@ -166,15 +166,16 @@
by (etac arg_cong 1);
qed "sum_case_weak_cong";
-val [p1,p2] = Goal "[| sum_case f1 f2 = sum_case g1 g2; \
- \ [| f1 = g1; f2 = g2 |] ==> P |] ==> P";
-by (cut_facts_tac [p1] 1);
-br p2 1;
-br ext 1;
-by (dres_inst_tac [("x","Inl x")] fun_cong 1);
+val [p1,p2] = Goal
+ "[| sum_case f1 f2 = sum_case g1 g2; \
+\ [| f1 = g1; f2 = g2 |] ==> P |] \
+\ ==> P";
+by (rtac p2 1);
+by (rtac ext 1);
+by (cut_inst_tac [("x","Inl x")] (p1 RS fun_cong) 1);
by (Asm_full_simp_tac 1);
-br ext 1;
-by (dres_inst_tac [("x","Inr x")] fun_cong 1);
+by (rtac ext 1);
+by (cut_inst_tac [("x","Inr x")] (p1 RS fun_cong) 1);
by (Asm_full_simp_tac 1);
qed "sum_case_inject";