Fixed several bugs concerning arbitrarily branching datatypes.
authorberghofe
Fri Oct 26 23:17:49 2001 +0200 (2001-10-26)
changeset 11951381135c295ef
parent 11950 9bd6e8e62a06
child 11952 b10f1e8862f4
Fixed several bugs concerning arbitrarily branching datatypes.
src/HOL/Tools/datatype_rep_proofs.ML
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Fri Oct 26 19:06:53 2001 +0200
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Fri Oct 26 23:17:49 2001 +0200
     1.3 @@ -438,7 +438,7 @@
     1.4  
     1.5          val inj_thm = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5)
     1.6            (HOLogic.mk_Trueprop (mk_conj ind_concl1))) (fn _ =>
     1.7 -            [indtac induction 1,
     1.8 +            [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
     1.9               REPEAT (EVERY
    1.10                 [rtac allI 1, rtac impI 1,
    1.11                  exh_tac (exh_thm_of dt_info) 1,
    1.12 @@ -448,12 +448,12 @@
    1.13                     REPEAT (dresolve_tac [In0_inject, In1_inject] 1),
    1.14                     (eresolve_tac [In0_not_In1 RS notE, In1_not_In0 RS notE] 1)
    1.15                     ORELSE (EVERY
    1.16 -                     [REPEAT (etac Scons_inject 1),
    1.17 -                      REPEAT (dresolve_tac
    1.18 -                        (inj_thms' @ [Leaf_inject, Lim_inject, Inl_inject, Inr_inject]) 1),
    1.19 +                     [REPEAT (eresolve_tac (Scons_inject :: sum_case_inject ::
    1.20 +                        map make_elim (inj_thms' @
    1.21 +                          [Leaf_inject, Lim_inject, Inl_inject, Inr_inject])) 1),
    1.22                        REPEAT ((EVERY [etac allE 1, dtac mp 1, atac 1]) ORELSE
    1.23                                (dtac inj_fun_lemma 1 THEN atac 1)),
    1.24 -                      TRY (hyp_subst_tac 1),
    1.25 +                      REPEAT (hyp_subst_tac 1),
    1.26                        rtac refl 1])])])]);
    1.27  
    1.28          val inj_thms'' = map (fn r => r RS datatype_injI)
    1.29 @@ -464,7 +464,7 @@
    1.30  	      (cterm_of (Theory.sign_of thy5)
    1.31  	       (HOLogic.mk_Trueprop (mk_conj ind_concl2)))
    1.32  	      (fn _ =>
    1.33 -	       [indtac induction 1,
    1.34 +	       [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
    1.35  		rewrite_goals_tac (o_def :: rewrites),
    1.36  		REPEAT (EVERY
    1.37  			[resolve_tac rep_intrs 1,