# HG changeset patch
# User berghofe
# Date 1004131069 -7200
# Node ID 381135c295effa84f86a64bc840d1cd414d84103
# Parent  9bd6e8e62a0661f5f7aa85c407723fe1d86dd32d
Fixed several bugs concerning arbitrarily branching datatypes.

diff -r 9bd6e8e62a06 -r 381135c295ef src/HOL/Tools/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Fri Oct 26 19:06:53 2001 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Fri Oct 26 23:17:49 2001 +0200
@@ -438,7 +438,7 @@
 
         val inj_thm = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5)
           (HOLogic.mk_Trueprop (mk_conj ind_concl1))) (fn _ =>
-            [indtac induction 1,
+            [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
              REPEAT (EVERY
                [rtac allI 1, rtac impI 1,
                 exh_tac (exh_thm_of dt_info) 1,
@@ -448,12 +448,12 @@
                    REPEAT (dresolve_tac [In0_inject, In1_inject] 1),
                    (eresolve_tac [In0_not_In1 RS notE, In1_not_In0 RS notE] 1)
                    ORELSE (EVERY
-                     [REPEAT (etac Scons_inject 1),
-                      REPEAT (dresolve_tac
-                        (inj_thms' @ [Leaf_inject, Lim_inject, Inl_inject, Inr_inject]) 1),
+                     [REPEAT (eresolve_tac (Scons_inject :: sum_case_inject ::
+                        map make_elim (inj_thms' @
+                          [Leaf_inject, Lim_inject, Inl_inject, Inr_inject])) 1),
                       REPEAT ((EVERY [etac allE 1, dtac mp 1, atac 1]) ORELSE
                               (dtac inj_fun_lemma 1 THEN atac 1)),
-                      TRY (hyp_subst_tac 1),
+                      REPEAT (hyp_subst_tac 1),
                       rtac refl 1])])])]);
 
         val inj_thms'' = map (fn r => r RS datatype_injI)
@@ -464,7 +464,7 @@
 	      (cterm_of (Theory.sign_of thy5)
 	       (HOLogic.mk_Trueprop (mk_conj ind_concl2)))
 	      (fn _ =>
-	       [indtac induction 1,
+	       [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
 		rewrite_goals_tac (o_def :: rewrites),
 		REPEAT (EVERY
 			[resolve_tac rep_intrs 1,