# HG changeset patch
# User nipkow
# Date 862918413 -7200
# Node ID 00fb015d27aa94b4d0f986b2ba7f937b75316d98
# Parent  dfc1d659f9680ea056001a00c0380b3e5874fe88
Stupid bug in induct_tac caused warning to always appear.

diff -r dfc1d659f968 -r 00fb015d27aa src/HOL/datatype.ML
--- 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"),