# HG changeset patch
# User blanchet
# Date 1406897037 -7200
# Node ID a35d2d26d66e995a7d00c0dca43b658f502a0b96
# Parent  25d498554c483ee456b8bf2792964ea355fce2d6
tentatively took out 'fastforce' from the set of tried methods -- it seems to be largely subsumed and is hard to silence

diff -r 25d498554c48 -r a35d2d26d66e src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -116,7 +116,7 @@
   * (term, string) atp_step list * thm
 
 val basic_systematic_methods = [Metis_Method (NONE, NONE), Meson_Method, Blast_Method, SATx_Method]
-val simp_based_methods = [Auto_Method, Simp_Method, Fastforce_Method, Force_Method]
+val simp_based_methods = [Auto_Method, Simp_Method, Force_Method]
 val basic_arith_methods = [Linarith_Method, Presburger_Method, Algebra_Method]
 
 val arith_methods = basic_arith_methods @ simp_based_methods @ basic_systematic_methods
diff -r 25d498554c48 -r a35d2d26d66e src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -18,7 +18,6 @@
     Simp_Method |
     Simp_Size_Method |
     Auto_Method |
-    Fastforce_Method |
     Force_Method |
     Linarith_Method |
     Presburger_Method |
@@ -57,7 +56,6 @@
   Simp_Method |
   Simp_Size_Method |
   Auto_Method |
-  Fastforce_Method |
   Force_Method |
   Linarith_Method |
   Presburger_Method |
@@ -94,7 +92,6 @@
       | Simp_Method => if null ss then "simp" else "simp add:"
       | Simp_Size_Method => "simp add: " ^ short_thm_name ctxt @{thm size_ne_size_imp_ne}
       | Auto_Method => "auto"
-      | Fastforce_Method => "fastforce"
       | Force_Method => "force"
       | Linarith_Method => "linarith"
       | Presburger_Method => "presburger"
@@ -128,15 +125,13 @@
       SATx_Method => SAT.satx_tac ctxt
     | Blast_Method => blast_tac ctxt
     | Auto_Method => K (Clasimp.auto_tac (silence_methods ctxt))
-    | Fastforce_Method => Clasimp.fast_force_tac (silence_methods ctxt)
     | Force_Method => Clasimp.force_tac (silence_methods ctxt)
     | Linarith_Method =>
       let val ctxt = Config.put Lin_Arith.verbose false ctxt in Lin_Arith.tac ctxt end
     | Presburger_Method => Cooper.tac true [] [] ctxt
     | Algebra_Method => Groebner.algebra_tac [] [] ctxt))
 
-val simp_based_methods =
-  [Simp_Method, Simp_Size_Method, Auto_Method, Fastforce_Method, Force_Method]
+val simp_based_methods = [Simp_Method, Simp_Size_Method, Auto_Method, Force_Method]
 
 fun thms_influence_proof_method ctxt meth ths =
   not (member (op =) simp_based_methods meth) orelse
diff -r 25d498554c48 -r a35d2d26d66e src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -163,8 +163,7 @@
 
 fun bunches_of_proof_methods smt_proofs needs_full_types desperate_lam_trans =
   [[Simp_Method, Auto_Method, Blast_Method, Linarith_Method],
-   [Fastforce_Method, Meson_Method,
-    Metis_Method (if needs_full_types then SOME full_typesN else NONE, NONE),
+   [Meson_Method, Metis_Method (if needs_full_types then SOME full_typesN else NONE, NONE),
     Force_Method, Presburger_Method],
     (if needs_full_types then
        [Metis_Method (NONE, NONE),