# HG changeset patch
# User blanchet
# Date 1406757176 -7200
# Node ID 9ea51eddf81c5ca26b506db013967850b1a42b33
# Parent  668322cd58f47c3e1582f5b7c42e16bd0e41ccbb
put faster proof methods first

diff -r 668322cd58f4 -r 9ea51eddf81c src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Wed Jul 30 23:52:56 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Wed Jul 30 23:52:56 2014 +0200
@@ -184,9 +184,9 @@
   | _ => "Try this")
 
 fun bunch_of_proof_methods smt_proofs needs_full_types desperate_lam_trans =
-  [Metis_Method (if needs_full_types then SOME full_typesN else NONE, NONE),
-   Auto_Method, Simp_Method, Fastforce_Method, Force_Method, Meson_Method, Blast_Method,
-   Linarith_Method, Presburger_Method] @
+  [Simp_Method, Auto_Method, Fastforce_Method, Blast_Method, Meson_Method,
+   Metis_Method (if needs_full_types then SOME full_typesN else NONE, NONE),
+   Force_Method, Linarith_Method, Presburger_Method] @
   (if needs_full_types then
      [Metis_Method (SOME really_full_type_enc, NONE),
       Metis_Method (SOME full_typesN, SOME desperate_lam_trans),