diff -r ecf5826ba234 -r 4ae52c60603a src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Aug 28 23:48:46 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Aug 28 23:57:26 2014 +0200
@@ -128,7 +128,7 @@
   * (term, string) atp_step list * thm
 
 val basic_systematic_methods = [Metis_Method (NONE, NONE), Meson_Method, Blast_Method, SATx_Method]
-val basic_simp_based_methods = [Auto_Method, Simp_Method, Force_Method]
+val basic_simp_based_methods = [Auto_Method, Simp_Method, Fastforce_Method, Force_Method]
 val basic_arith_methods = [Linarith_Method, Presburger_Method, Algebra_Method]
 
 val arith_methods = basic_arith_methods @ basic_simp_based_methods @ basic_systematic_methods
@@ -137,7 +137,7 @@
   basic_systematic_methods @ basic_arith_methods @ basic_simp_based_methods @
   [Metis_Method (SOME full_typesN, NONE), Metis_Method (SOME no_typesN, NONE)]
 val rewrite_methods = basic_simp_based_methods @ basic_systematic_methods @ basic_arith_methods
-fun skolem_methods_of z3 = (basic_systematic_methods, [Skolem_Method]) |> z3 ? swap |> op @
+fun skolem_methods_of z3 = basic_systematic_methods |> z3 ? cons Moura_Method
 
 fun isar_proof_text ctxt debug isar_proofs smt_proofs isar_params
     (one_line_params as ((used_facts, (_, one_line_play)), banner, subgoal, subgoal_count)) =