# HG changeset patch
# User wenzelm
# Date 975519760 -3600
# Node ID 92cd56dfc17e78d8002d3e2a8fa624341b9d02a7
# Parent  fdec07d4f04759a3602de1be0ddc092754b135d1
resolveq_cases_tac moved here from Pure/Isar/method.ML;
induct: proper handling of non-consumed facts;

diff -r fdec07d4f047 -r 92cd56dfc17e src/HOL/Tools/induct_method.ML
--- a/src/HOL/Tools/induct_method.ML	Wed Nov 29 18:41:43 2000 +0100
+++ b/src/HOL/Tools/induct_method.ML	Wed Nov 29 18:42:40 2000 +0100
@@ -91,6 +91,22 @@
 end;
 
 
+(* resolution and cases *)
+
+local
+
+fun gen_resolveq_tac tac rules i st =
+  Seq.flat (Seq.map (fn rule => tac rule i st) rules);
+
+in
+
+fun resolveq_cases_tac make tac = gen_resolveq_tac (fn (rule, (cases, facts)) => fn i => fn st =>
+  Seq.map (rpair (make rule cases))
+    ((Method.insert_tac facts THEN' tac THEN' Tactic.rtac rule) i st));
+
+end;
+
+
 
 (** cases method **)
 
@@ -161,7 +177,7 @@
     fun prep_rule (thm, (cases, n)) = Seq.map (apsnd (rpair (drop (n, facts))) o cond_simp cases)
       (Method.multi_resolves (take (n, facts)) [thm]);
   in
-    Method.resolveq_cases_tac (RuleCases.make open_parms)
+    resolveq_cases_tac (RuleCases.make open_parms) (K all_tac)
       (Seq.flat (Seq.map prep_rule (Seq.of_list rules)))
   end;
 
@@ -277,11 +293,10 @@
 
     fun prep_rule (thm, (cases, n)) =
       Seq.map (rpair (cases, drop (n, facts))) (Method.multi_resolves (take (n, facts)) [thm]);
-    val tac = Method.resolveq_cases_tac (rulify_cases cert open_parms)
+    val tac = resolveq_cases_tac (rulify_cases cert open_parms) atomize_tac
       (Seq.flat (Seq.map prep_rule (Seq.of_list rules)));
   in
-    (fn i => Seq.THEN (atomize_tac i, tac i)) THEN_ALL_NEW_CASES
-      (rulify_tac THEN' (if stripped then weak_strip_tac else K all_tac))
+    tac THEN_ALL_NEW_CASES (rulify_tac THEN' (if stripped then weak_strip_tac else K all_tac))
   end;
 
 in