Stupid bug in induct_tac caused warning to always appear.

--- a/src/HOL/datatype.ML	Tue May 06 12:55:07 1997 +0200
+++ b/src/HOL/datatype.ML	Tue May 06 13:33:33 1997 +0200
@@ -841,10 +841,11 @@
      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"),