diff -r 467d5b34e1f5 -r b02749a3b0ac src/HOL/Tools/Metis/metis_tactics.ML
--- 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]