# HG changeset patch
# User wenzelm
# Date 952113658 -3600
# Node ID 4c117393e4e68379c4b2e94cc93bd52515cb3466
# Parent  7896bcbd8641e6fb2b65c5935c2cd1aefc904611
added multi_resolveq, resolveq_tac;

diff -r 7896bcbd8641 -r 4c117393e4e6 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Fri Mar 03 18:26:19 2000 +0100
+++ b/src/Pure/Isar/method.ML	Fri Mar 03 21:00:58 2000 +0100
@@ -37,6 +37,8 @@
   val fold: thm list -> Proof.method
   val multi_resolve: thm list -> thm -> thm Seq.seq
   val multi_resolves: thm list -> thm list -> thm Seq.seq
+  val multi_resolveq: thm list -> thm Seq.seq -> thm Seq.seq
+  val resolveq_tac: thm Seq.seq -> int -> tactic
   val rule_tac: thm list -> thm list -> int -> tactic
   val rule: thm list -> Proof.method
   val erule: thm list -> Proof.method
@@ -245,21 +247,24 @@
 in
 
 val multi_resolve = multi_res 1;
-fun multi_resolves facts rules = Seq.flat (Seq.map (multi_resolve facts) (Seq.of_list rules));
+fun multi_resolveq facts rules = Seq.flat (Seq.map (multi_resolve facts) rules);
+fun multi_resolves facts = multi_resolveq facts o Seq.of_list;
 
 end;
 
 
 (* 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.resolve_tac;
+
+
 local
 
 fun gen_rule_tac tac rules [] = tac rules
-  | gen_rule_tac tac erules facts =
-      let
-        val rules = multi_resolves facts erules;
-        fun tactic i state = Seq.flat (Seq.map (fn rule => tac [rule] i state) rules);
-      in tactic end;
+  | gen_rule_tac tac erules facts = gen_resolveq_tac tac (multi_resolves facts erules);
 
 fun gen_rule tac rules = METHOD (FINDGOAL o tac rules);