src/Provers/classical.ML
changeset 18223 20830cb4428c
parent 18015 1cd8174b7df0
child 18374 598e7fd7438b
     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)