# HG changeset patch
# User berghofe
# Date 1197912776 -3600
# Node ID 2495389bc1f5a656acc04469dffcfb05ddd19fda
# Parent  8b2ddc6e7be19243e447b2f368d529e045ea6156
Adapted to changes in interface of indtac.

diff -r 8b2ddc6e7be1 -r 2495389bc1f5 src/HOL/Tools/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Mon Dec 17 18:31:52 2007 +0100
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Mon Dec 17 18:32:56 2007 +0100
@@ -404,7 +404,7 @@
 
         val inj_thm = Goal.prove_global thy5 [] []
           (HOLogic.mk_Trueprop (mk_conj ind_concl1)) (fn _ => EVERY
-            [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
+            [(indtac induction [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
              REPEAT (EVERY
                [rtac allI 1, rtac impI 1,
                 exh_tac (exh_thm_of dt_info) 1,
@@ -430,7 +430,7 @@
         val elem_thm = 
             Goal.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2))
               (fn _ =>
-               EVERY [(indtac induction THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
+               EVERY [(indtac induction [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
                 rewrite_goals_tac rewrites,
                 REPEAT ((resolve_tac rep_intrs THEN_ALL_NEW
                   ((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]);
@@ -466,7 +466,7 @@
     val iso_thms = if length descr = 1 then [] else
       Library.drop (length newTs, split_conj_thm
         (Goal.prove_global thy5 [] [] iso_t (fn _ => EVERY
-           [(indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
+           [(indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
             REPEAT (rtac TrueI 1),
             rewrite_goals_tac (mk_meta_eq choice_eq ::
               symmetric (mk_meta_eq expand_fun_eq) :: range_eqs),
@@ -608,7 +608,7 @@
       (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
       (fn prems => EVERY
         [rtac indrule_lemma' 1,
-         (indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
+         (indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
          EVERY (map (fn (prem, r) => (EVERY
            [REPEAT (eresolve_tac Abs_inverse_thms 1),
             simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1,