| changeset 43169 | b02749a3b0ac |
| parent 43160 | d4f347508cd4 |
| child 43184 | b16693484c5d |
--- a/src/HOL/Tools/Metis/metis_tactics.ML Mon Jun 06 20:36:34 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_tactics.ML Mon Jun 06 20:36:34 2011 +0200 @@ -206,8 +206,8 @@ Meson.MESON (preskolem_tac ctxt) (maps neg_clausify) tac ctxt i st0 end -val metis_modes = [HO, FT] -val metisF_modes = [FO, FT] +val metis_modes = [HO, MX] +val metisF_modes = [FO, MX] val metisFT_modes = [FT] val metisHO_modes = [HO] val metisX_modes = [MX]