# HG changeset patch
# User wenzelm
# Date 1012069035 -3600
# Node ID c6a8e310aec55b829db5a8aa74d8cb3cd20fc3b6
# Parent  e874962869347f3adb34a15d33fd978bdec760a2
cases: really append cases_default;
cases/induct method: DETERM;

diff -r e87496286934 -r c6a8e310aec5 src/Provers/induct_method.ML
--- a/src/Provers/induct_method.ML	Sat Jan 26 19:15:51 2002 +0100
+++ b/src/Provers/induct_method.ML	Sat Jan 26 19:17:15 2002 +0100
@@ -101,15 +101,13 @@
         |> Drule.cterm_instantiate) r |> rpair (RuleCases.get r);
 
     val ruleq =
-      (case (facts, insts, opt_rule) of
-        ([], [], None) => Seq.single (RuleCases.add Data.cases_default)
-      | (_, _, None) =>
-          let val rules = find_casesS ctxt facts @ find_casesT ctxt insts in
-            if null rules then error "Unable to figure out cases rule" else ();
+      (case opt_rule of
+        None =>
+          let val rules = find_casesS ctxt facts @ find_casesT ctxt insts @ [Data.cases_default] in
             Method.trace ctxt rules;
             Seq.flat (Seq.map (Seq.try inst_rule) (Seq.of_list rules))
           end
-      | (_, _, Some r) => Seq.single (inst_rule r));
+      | Some r => Seq.single (inst_rule r));
 
     fun prep_rule (th, (cases, n)) = Seq.map (apsnd (rpair (drop (n, facts))) o rpair cases)
       (Method.multi_resolves (take (n, facts)) [th]);
@@ -117,7 +115,7 @@
 
 in
 
-val cases_meth = Method.METHOD_CASES o (HEADGOAL oo cases_tac);
+val cases_meth = Method.METHOD_CASES o ((Seq.DETERM o HEADGOAL) oo cases_tac);
 
 end;
 
@@ -291,7 +289,7 @@
 
 in
 
-val induct_meth = Method.RAW_METHOD_CASES o (HEADGOAL oo induct_tac);
+val induct_meth = Method.RAW_METHOD_CASES o ((Seq.DETERM o HEADGOAL) oo induct_tac);
 
 end;