src/HOL/Tools/Datatype/datatype.ML
changeset 35625 9c818cab0dd0
parent 35410 1ea89d2a1bd4
child 35742 eb8d2f668bfc
     1.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Sun Mar 07 11:57:16 2010 +0100
     1.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Sun Mar 07 12:19:47 2010 +0100
     1.3 @@ -417,7 +417,7 @@
     1.4  
     1.5          val inj_thm = Skip_Proof.prove_global thy5 [] []
     1.6            (HOLogic.mk_Trueprop (mk_conj ind_concl1)) (fn _ => EVERY
     1.7 -            [(indtac induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
     1.8 +            [(indtac induct [] THEN_ALL_NEW Object_Logic.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 @@ -443,7 +443,7 @@
    1.13          val elem_thm = 
    1.14              Skip_Proof.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2))
    1.15                (fn _ =>
    1.16 -               EVERY [(indtac induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
    1.17 +               EVERY [(indtac induct [] THEN_ALL_NEW Object_Logic.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 @@ -479,7 +479,7 @@
    1.22      val iso_thms = if length descr = 1 then [] else
    1.23        drop (length newTs) (split_conj_thm
    1.24          (Skip_Proof.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 Object_Logic.atomize_prems_tac) 1,
    1.27              REPEAT (rtac TrueI 1),
    1.28              rewrite_goals_tac (mk_meta_eq @{thm choice_eq} ::
    1.29                symmetric (mk_meta_eq @{thm expand_fun_eq}) :: range_eqs),
    1.30 @@ -617,7 +617,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 Object_Logic.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,