src/Pure/Isar/calculation.ML
changeset 18223 20830cb4428c
parent 17384 c01de5939f5b
child 18377 0e1d025d57b3
     1.1 --- a/src/Pure/Isar/calculation.ML	Tue Nov 22 19:34:40 2005 +0100
     1.2 +++ b/src/Pure/Isar/calculation.ML	Tue Nov 22 19:34:41 2005 +0100
     1.3 @@ -110,7 +110,7 @@
     1.4  (* symmetry *)
     1.5  
     1.6  fun gen_symmetric get_sym = Drule.rule_attribute (fn x => fn th =>
     1.7 -  (case Seq.chop (2, Method.multi_resolves [th] (get_sym x)) of
     1.8 +  (case Seq.chop (2, Drule.multi_resolves [th] (get_sym x)) of
     1.9      ([th'], _) => th'
    1.10    | ([], _) => raise THM ("symmetric: no unifiers", 1, [th])
    1.11    | _ => raise THM ("symmetric: multiple unifiers", 1, [th])));
    1.12 @@ -170,7 +170,7 @@
    1.13        | NONE =>
    1.14            (case ths of [] => NetRules.rules (#1 (get_local_rules state))
    1.15            | th :: _ => NetRules.retrieve (#1 (get_local_rules state)) (strip_assums_concl th)))
    1.16 -      |> Seq.of_list |> Seq.maps (Method.multi_resolve ths)
    1.17 +      |> Seq.of_list |> Seq.maps (Drule.multi_resolve ths)
    1.18        |> Seq.filter (not o projection ths);
    1.19  
    1.20      val facts = Proof.the_facts (assert_sane final state);