1.1 --- a/src/Provers/induct_method.ML	Sat Jan 26 19:15:51 2002 +0100
     1.2 +++ b/src/Provers/induct_method.ML	Sat Jan 26 19:17:15 2002 +0100
     1.3 @@ -101,15 +101,13 @@
     1.4          |> Drule.cterm_instantiate) r |> rpair (RuleCases.get r);
     1.5  
     1.6      val ruleq =
     1.7 -      (case (facts, insts, opt_rule) of
     1.8 -        ([], [], None) => Seq.single (RuleCases.add Data.cases_default)
     1.9 -      | (_, _, None) =>
    1.10 -          let val rules = find_casesS ctxt facts @ find_casesT ctxt insts in
    1.11 -            if null rules then error "Unable to figure out cases rule" else ();
    1.12 +      (case opt_rule of
    1.13 +        None =>
    1.14 +          let val rules = find_casesS ctxt facts @ find_casesT ctxt insts @ [Data.cases_default] in
    1.15              Method.trace ctxt rules;
    1.16              Seq.flat (Seq.map (Seq.try inst_rule) (Seq.of_list rules))
    1.17            end
    1.18 -      | (_, _, Some r) => Seq.single (inst_rule r));
    1.19 +      | Some r => Seq.single (inst_rule r));
    1.20  
    1.21      fun prep_rule (th, (cases, n)) = Seq.map (apsnd (rpair (drop (n, facts))) o rpair cases)
    1.22        (Method.multi_resolves (take (n, facts)) [th]);
    1.23 @@ -117,7 +115,7 @@
    1.24  
    1.25  in
    1.26  
    1.27 -val cases_meth = Method.METHOD_CASES o (HEADGOAL oo cases_tac);
    1.28 +val cases_meth = Method.METHOD_CASES o ((Seq.DETERM o HEADGOAL) oo cases_tac);
    1.29  
    1.30  end;
    1.31  
    1.32 @@ -291,7 +289,7 @@
    1.33  
    1.34  in
    1.35  
    1.36 -val induct_meth = Method.RAW_METHOD_CASES o (HEADGOAL oo induct_tac);
    1.37 +val induct_meth = Method.RAW_METHOD_CASES o ((Seq.DETERM o HEADGOAL) oo induct_tac);
    1.38  
    1.39  end;
    1.40