# HG changeset patch
# User paulson
# Date 933064186 -7200
# Node ID 67c6706578ed8312c71d0538009b9a07bba0f9d7
# Parent  f9aa63a5a8b65a7f22dc048ef3d9b361fcd3819b
tidied

diff -r f9aa63a5a8b6 -r 67c6706578ed src/HOL/Sum.ML
--- 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";