--- 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