# HG changeset patch
# User wenzelm
# Date 975370237 -3600
# Node ID b92c228660e491dda65e47e0efd1f4a16c7cda83
# Parent  a0483268262d7bc621803aa2e83d1bcdc7e403b3
resolveq_cases_tac: insert facts;

diff -r a0483268262d -r b92c228660e4 src/Pure/Isar/method.ML
--- 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 *)