Drule.multi_resolves;

--- a/src/Provers/classical.ML	Tue Nov 22 19:34:40 2005 +0100
+++ b/src/Provers/classical.ML	Tue Nov 22 19:34:41 2005 +0100
@@ -985,7 +985,7 @@
     val [rules1, rules2, rules4] = ContextRules.find_rules false facts goal ctxt;
     val rules3 = ContextRules.find_rules_netpair true facts goal xtra_netpair;
     val rules = rules1 @ rules2 @ rules3 @ rules4;
-    val ruleq = Method.multi_resolves facts rules;
+    val ruleq = Drule.multi_resolves facts rules;
   in
     Method.trace ctxt rules;
     fn st => Seq.flat (Seq.map (fn rule => Tactic.rtac rule i st) ruleq)

--- a/src/Pure/Isar/calculation.ML	Tue Nov 22 19:34:40 2005 +0100
+++ b/src/Pure/Isar/calculation.ML	Tue Nov 22 19:34:41 2005 +0100
@@ -110,7 +110,7 @@
 (* symmetry *)
 
 fun gen_symmetric get_sym = Drule.rule_attribute (fn x => fn th =>
-  (case Seq.chop (2, Method.multi_resolves [th] (get_sym x)) of
+  (case Seq.chop (2, Drule.multi_resolves [th] (get_sym x)) of
     ([th'], _) => th'
   | ([], _) => raise THM ("symmetric: no unifiers", 1, [th])
   | _ => raise THM ("symmetric: multiple unifiers", 1, [th])));
@@ -170,7 +170,7 @@
       | NONE =>
           (case ths of [] => NetRules.rules (#1 (get_local_rules state))
           | th :: _ => NetRules.retrieve (#1 (get_local_rules state)) (strip_assums_concl th)))
-      |> Seq.of_list |> Seq.maps (Method.multi_resolve ths)
+      |> Seq.of_list |> Seq.maps (Drule.multi_resolve ths)
       |> Seq.filter (not o projection ths);
 
     val facts = Proof.the_facts (assert_sane final state);