# HG changeset patch
# User nipkow
# Date 862848571 -7200
# Node ID 1a5bfa2ab1d1afd861b5e1fa94c0f64b9f18d16f
# Parent  86f8e75c2296ffc1676f12fd3453cbf1eaf14a67
Cosmetic update of induct_tac; test first now.

diff -r 86f8e75c2296 -r 1a5bfa2ab1d1 src/HOL/datatype.ML
--- a/src/HOL/datatype.ML	Mon May 05 13:24:38 1997 +0200
+++ b/src/HOL/datatype.ML	Mon May 05 18:09:31 1997 +0200
@@ -840,10 +840,11 @@
      fun const s = Const(s, the(Sign.const_type sign s))
      val case_rewrites = map (fn c => get_fact thy (ty^"_case_"^c)) cl
      val {nchotomy,case_cong} = case_thms sign case_rewrites itac
-     fun induct_tac a i = itac a i THEN
+     fun induct_tac a i =
            COND (Datatype.occs_in_prems a i)
              (warning "Induction variable occurs also among premises!";
               all_tac) all_tac
+           THEN itac a i
  in
   (ty, {constructors = map(fn s => const s handle _ => const("op "^s)) cl,
         case_const = const (ty^"_case"),