changeset 40262 | 8403085384eb |
parent 40259 | c0e34371c2e2 |
child 40665 | 1a65f0c74827 |
--- a/src/HOL/Tools/Metis/metis_tactics.ML Fri Oct 29 12:49:05 2010 +0200 +++ b/src/HOL/Tools/Metis/metis_tactics.ML Fri Oct 29 12:49:05 2010 +0200 @@ -157,7 +157,7 @@ (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty) else Meson.MESON (preskolem_tac ctxt) (maps neg_clausify) - (fn cls => resolve_tac (FOL_SOLVE mode ctxt [] (cls @ ths)) 1) + (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i st0 end