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