author | blanchet |
Mon, 26 Apr 2010 21:18:20 +0200 | |
changeset 36401 | 31252c4d4923 |
parent 36400 | c5bae529f967 |
child 36402 | 1b20805974c7 |
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Apr 26 21:17:41 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Apr 26 21:18:20 2010 +0200 @@ -721,7 +721,7 @@ if exists_type type_has_topsort (prop_of st0) then raise METIS "Metis: Proof state contains the universal sort {}" else - (Meson.MESON neg_clausify + (Meson.MESON (maps neg_clausify) (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i THEN Meson_Tactic.expand_defs_tac st0) st0 end