src/Pure/Isar/method.ML

   val insert_facts: Proof.method
   val unfold: thm list -> Proof.method
   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
   val drule: thm list -> Proof.method
   val frule: thm list -> Proof.method

   | multi_res i (th :: ths) rule = Seq.flat (Seq.map (res th i) (multi_res (i + 1) ths rule));
 
 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);
 
 fun gen_rule' tac arg_rules ctxt = METHOD (fn facts =>
   let val rules =