--- a/src/Pure/Isar/method.ML Tue Nov 28 01:10:22 2000 +0100
+++ b/src/Pure/Isar/method.ML Tue Nov 28 01:10:37 2000 +0100
@@ -45,7 +45,8 @@
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) Seq.seq -> int -> thm -> (thm * (string * RuleCases.T) list) Seq.seq
+ -> (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
@@ -314,8 +315,8 @@
val resolveq_tac = gen_resolveq_tac Tactic.rtac;
-fun resolveq_cases_tac make = gen_resolveq_tac (fn (rule, cases) => fn i => fn st =>
- Seq.map (rpair (make rule cases)) (Tactic.rtac rule i st));
+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 *)