src/HOL/datatype.ML

  let val sign = sign_of thy
      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 =
-           COND (Datatype.occs_in_prems a i)
-             (warning "Induction variable occurs also among premises!";
-              all_tac) all_tac
-           THEN itac a i
+           STATE(fn st =>
+             (if Datatype.occs_in_prems a i st
+              then warning "Induction variable occurs also among premises!"
+              else ();
+              itac a i))
  in
   (ty, {constructors = map(fn s => const s handle _ => const("op "^s)) cl,
         case_const = const (ty^"_case"),
         case_rewrites = map mk_rw case_rewrites,
         induct_tac = induct_tac,