--- 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);