# HG changeset patch
# User wenzelm
# Date 975519703 -3600
# Node ID fdec07d4f04759a3602de1be0ddc092754b135d1
# Parent  abe2322fa422b102bf36e811b8d574f2891889b7
resolveq(_cases)_tac moved to HOL/Tools/induct_method.ML;

diff -r abe2322fa422 -r fdec07d4f047 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Wed Nov 29 17:24:20 2000 +0100
+++ b/src/Pure/Isar/method.ML	Wed Nov 29 18:41:43 2000 +0100
@@ -43,10 +43,6 @@
   val atomize_goal: thm list -> int -> thm -> thm
   val multi_resolve: thm list -> thm -> thm Seq.seq
   val multi_resolves: thm list -> thm list -> thm Seq.seq
-  val resolveq_tac: thm Seq.seq -> int -> tactic
-  val resolveq_cases_tac: (thm -> string list -> (string * RuleCases.T) list)
-    -> (thm * (string list * thm list)) Seq.seq
-    -> int -> thm -> (thm * (string * RuleCases.T) list) Seq.seq
   val rule_tac: thm list -> thm list -> int -> tactic
   val erule_tac: thm list -> thm list -> int -> tactic
   val some_rule_tac: thm list -> Proof.context -> thm list -> int -> tactic
@@ -308,23 +304,13 @@
 end;
 
 
-(* general rule *)
-
-fun gen_resolveq_tac tac rules i st =
-  Seq.flat (Seq.map (fn rule => tac rule i st) rules);
-
-val resolveq_tac = gen_resolveq_tac Tactic.rtac;
-
-fun resolveq_cases_tac make = gen_resolveq_tac (fn (rule, (cases, facts)) => fn i => fn st =>
-  Seq.map (rpair (make rule cases)) ((insert_tac facts i THEN Tactic.rtac rule i) st));
-
-
 (* simple rule *)
 
 local
 
-fun gen_rule_tac tac rules [] = tac rules
-  | gen_rule_tac tac erules facts = gen_resolveq_tac (tac o single) (multi_resolves facts erules);
+fun gen_rule_tac tac rules [] i st = tac rules i st
+  | gen_rule_tac tac erules facts i st =
+      Seq.flat (Seq.map (fn rule => (tac o single) rule i st) (multi_resolves facts erules));
 
 fun gen_some_rule_tac tac arg_rules ctxt facts =
   let val rules =