Adapted to changes in interface of indtac.
authorberghofe
Mon Dec 17 18:32:56 2007 +0100 (2007-12-17)
changeset 256782495389bc1f5
parent 25677 8b2ddc6e7be1
child 25679 b77f797b528a
Adapted to changes in interface of indtac.
src/HOL/Tools/datatype_rep_proofs.ML
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Mon Dec 17 18:31:52 2007 +0100
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Mon Dec 17 18:32:56 2007 +0100
     1.3 @@ -404,7 +404,7 @@
     1.4  
     1.5          val inj_thm = Goal.prove_global thy5 [] []
     1.6            (HOLogic.mk_Trueprop (mk_conj ind_concl1)) (fn _ => EVERY
     1.7 -            [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
     1.8 +            [(indtac induction [] THEN_ALL_NEW ObjectLogic.atomize_prems_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 @@ -430,7 +430,7 @@
    1.13          val elem_thm = 
    1.14              Goal.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2))
    1.15                (fn _ =>
    1.16 -               EVERY [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
    1.17 +               EVERY [(indtac induction [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
    1.18                  rewrite_goals_tac rewrites,
    1.19                  REPEAT ((resolve_tac rep_intrs THEN_ALL_NEW
    1.20                    ((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]);
    1.21 @@ -466,7 +466,7 @@
    1.22      val iso_thms = if length descr = 1 then [] else
    1.23        Library.drop (length newTs, split_conj_thm
    1.24          (Goal.prove_global thy5 [] [] iso_t (fn _ => EVERY
    1.25 -           [(indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
    1.26 +           [(indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
    1.27              REPEAT (rtac TrueI 1),
    1.28              rewrite_goals_tac (mk_meta_eq choice_eq ::
    1.29                symmetric (mk_meta_eq expand_fun_eq) :: range_eqs),
    1.30 @@ -608,7 +608,7 @@
    1.31        (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
    1.32        (fn prems => EVERY
    1.33          [rtac indrule_lemma' 1,
    1.34 -         (indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
    1.35 +         (indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
    1.36           EVERY (map (fn (prem, r) => (EVERY
    1.37             [REPEAT (eresolve_tac Abs_inverse_thms 1),
    1.38              simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1,