1.1 --- a/src/HOL/Tools/induct_method.ML	Mon Mar 20 18:48:12 2000 +0100
     1.2 +++ b/src/HOL/Tools/induct_method.ML	Mon Mar 20 18:48:43 2000 +0100
     1.3 @@ -214,7 +214,7 @@
     1.4  
     1.5      val rules =
     1.6        (case (args, facts) of
     1.7 -        ((None, None), []) => [RuleCases.none case_split_thm]		(* FIXME add cases!? *)
     1.8 +        ((None, None), []) => [(case_split_thm, ["True", "False"])]
     1.9        | ((Some t, None), []) =>
    1.10            let val name = type_name t in
    1.11              (case lookup_casesT ctxt name of
    1.12 @@ -257,7 +257,7 @@
    1.13  
    1.14  fun (tac1 THEN_ALL_NEW_CASES tac2) i st =
    1.15    st |> Seq.THEN (tac1 i, (fn (st', cases) =>
    1.16 -    Seq.map (rpair cases) (ALLGOALS_RANGE tac2 i (i + nprems_of st' - nprems_of st) st')));
    1.17 +    Seq.map (rpair cases) (Seq.INTERVAL tac2 i (i + nprems_of st' - nprems_of st) st')));
    1.18  
    1.19  
    1.20  fun induct_rule ctxt t =
    1.21 @@ -311,7 +311,7 @@
    1.22  
    1.23      val rules =
    1.24        (case (args, facts) of
    1.25 -        (([], None), []) => [RuleCases.none nat_induct]		(* FIXME add cases!? *)
    1.26 +        (([], None), []) => []
    1.27        | ((insts, None), []) =>
    1.28            let val thms = map (induct_rule ctxt o last_elem) insts
    1.29            in [(inst_rule insts (join_rules thms), RuleCases.get (#2 (hd thms)))] end