Drule.multi_resolves;
authorwenzelm
Tue Nov 22 19:34:41 2005 +0100 (2005-11-22 ago)
changeset 1822320830cb4428c
parent 18222 a8ccacce3b52
child 18224 1b191bb611f4
Drule.multi_resolves;
src/Provers/classical.ML
src/Pure/Isar/calculation.ML
     1.1 --- a/src/Provers/classical.ML	Tue Nov 22 19:34:40 2005 +0100
     1.2 +++ b/src/Provers/classical.ML	Tue Nov 22 19:34:41 2005 +0100
     1.3 @@ -985,7 +985,7 @@
     1.4      val [rules1, rules2, rules4] = ContextRules.find_rules false facts goal ctxt;
     1.5      val rules3 = ContextRules.find_rules_netpair true facts goal xtra_netpair;
     1.6      val rules = rules1 @ rules2 @ rules3 @ rules4;
     1.7 -    val ruleq = Method.multi_resolves facts rules;
     1.8 +    val ruleq = Drule.multi_resolves facts rules;
     1.9    in
    1.10      Method.trace ctxt rules;
    1.11      fn st => Seq.flat (Seq.map (fn rule => Tactic.rtac rule i st) ruleq)
     2.1 --- a/src/Pure/Isar/calculation.ML	Tue Nov 22 19:34:40 2005 +0100
     2.2 +++ b/src/Pure/Isar/calculation.ML	Tue Nov 22 19:34:41 2005 +0100
     2.3 @@ -110,7 +110,7 @@
     2.4  (* symmetry *)
     2.5  
     2.6  fun gen_symmetric get_sym = Drule.rule_attribute (fn x => fn th =>
     2.7 -  (case Seq.chop (2, Method.multi_resolves [th] (get_sym x)) of
     2.8 +  (case Seq.chop (2, Drule.multi_resolves [th] (get_sym x)) of
     2.9      ([th'], _) => th'
    2.10    | ([], _) => raise THM ("symmetric: no unifiers", 1, [th])
    2.11    | _ => raise THM ("symmetric: multiple unifiers", 1, [th])));
    2.12 @@ -170,7 +170,7 @@
    2.13        | NONE =>
    2.14            (case ths of [] => NetRules.rules (#1 (get_local_rules state))
    2.15            | th :: _ => NetRules.retrieve (#1 (get_local_rules state)) (strip_assums_concl th)))
    2.16 -      |> Seq.of_list |> Seq.maps (Method.multi_resolve ths)
    2.17 +      |> Seq.of_list |> Seq.maps (Drule.multi_resolve ths)
    2.18        |> Seq.filter (not o projection ths);
    2.19  
    2.20      val facts = Proof.the_facts (assert_sane final state);