# HG changeset patch
# User blanchet
# Date 1391418858 -3600
# Node ID b84867d6550bf0cdedbbac29d354965b6d81b45b
# Parent  e887c074361414684bf48fb0de8870875ae99c2e
added a new version of 'metis' to the mix

diff -r e887c0743614 -r b84867d6550b src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 10:14:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 10:14:18 2014 +0100
@@ -117,7 +117,8 @@
 val datatype_methods = [Simp_Method, Simp_Size_Method]
 val metislike_methods0 =
   [Metis_Method (NONE, NONE), Simp_Method, Auto_Method, Arith_Method, Blast_Method,
-   Fastforce_Method, Force_Method, Algebra_Method, Meson_Method]
+   Fastforce_Method, Force_Method, Algebra_Method, Meson_Method,
+   Metis_Method (SOME no_typesN, NONE)]
 val rewrite_methods =
   [Auto_Method, Simp_Method, Fastforce_Method, Force_Method, Metis_Method (NONE, NONE),
    Meson_Method]