# HG changeset patch
# User wenzelm
# Date 953574523 -3600
# Node ID 3a45bc1ff175ec57a089d8154dec12e904a1e5f5
# Parent  3cbe48a112f793ec5ce52b8025538efc3d9dd936
tuned degenerate cases / induct;

diff -r 3cbe48a112f7 -r 3a45bc1ff175 src/HOL/Tools/induct_method.ML
--- a/src/HOL/Tools/induct_method.ML	Mon Mar 20 18:48:12 2000 +0100
+++ b/src/HOL/Tools/induct_method.ML	Mon Mar 20 18:48:43 2000 +0100
@@ -214,7 +214,7 @@
 
     val rules =
       (case (args, facts) of
-        ((None, None), []) => [RuleCases.none case_split_thm]		(* FIXME add cases!? *)
+        ((None, None), []) => [(case_split_thm, ["True", "False"])]
       | ((Some t, None), []) =>
           let val name = type_name t in
             (case lookup_casesT ctxt name of
@@ -257,7 +257,7 @@
 
 fun (tac1 THEN_ALL_NEW_CASES tac2) i st =
   st |> Seq.THEN (tac1 i, (fn (st', cases) =>
-    Seq.map (rpair cases) (ALLGOALS_RANGE tac2 i (i + nprems_of st' - nprems_of st) st')));
+    Seq.map (rpair cases) (Seq.INTERVAL tac2 i (i + nprems_of st' - nprems_of st) st')));
 
 
 fun induct_rule ctxt t =
@@ -311,7 +311,7 @@
 
     val rules =
       (case (args, facts) of
-        (([], None), []) => [RuleCases.none nat_induct]		(* FIXME add cases!? *)
+        (([], None), []) => []
       | ((insts, None), []) =>
           let val thms = map (induct_rule ctxt o last_elem) insts
           in [(inst_rule insts (join_rules thms), RuleCases.get (#2 (hd thms)))] end