# HG changeset patch
# User blanchet
# Date 1432799417 -7200
# Node ID 7d278b0617d3d109d7225e34eede85489e9ebec3
# Parent  3f429b7d8eb5c1e7d2321b03a37f22072918802a
took out Sledgehammer minimizer optimization that breaks things

diff -r 3f429b7d8eb5 -r 7d278b0617d3 src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Thu May 28 17:25:57 2015 +1000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Thu May 28 09:50:17 2015 +0200
@@ -38,10 +38,8 @@
 val slack = seconds 0.025
 
 fun minimized_isar_step ctxt time
-    (Prove (qs, xs, l, t, subproofs, (lfs0, gfs00), meths as meth :: _, comment)) =
+    (Prove (qs, xs, l, t, subproofs, (lfs0, gfs0), meths as meth :: _, comment)) =
   let
-    val gfs0 = filter (thms_influence_proof_method ctxt meth o thms_of_name ctxt) gfs00
-
     fun mk_step_lfs_gfs lfs gfs =
       Prove (qs, xs, l, t, subproofs, sort_facts (lfs, gfs), meths, comment)
 
diff -r 3f429b7d8eb5 -r 7d278b0617d3 src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Thu May 28 17:25:57 2015 +1000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Thu May 28 09:50:17 2015 +0200
@@ -37,7 +37,6 @@
   val proof_method_distinguishes_chained_and_direct : proof_method -> bool
   val string_of_proof_method : Proof.context -> string list -> proof_method -> string
   val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic
-  val thms_influence_proof_method : Proof.context -> proof_method -> thm list -> bool
   val string_of_play_outcome : play_outcome -> string
   val play_outcome_ord : play_outcome * play_outcome -> order
   val one_line_proof_text : Proof.context -> int -> one_line_params -> string
@@ -141,13 +140,6 @@
     | Presburger_Method => Cooper.tac true [] [] ctxt
     | Algebra_Method => Groebner.algebra_tac [] [] ctxt))
 
-val simp_based_methods = [Simp_Method, Simp_Size_Method, Auto_Method, Force_Method, Moura_Method]
-
-fun thms_influence_proof_method ctxt meth ths =
-  not (member (op =) simp_based_methods meth) orelse
-  (* unfortunate pointer comparison -- but it's always safe to consider a theorem useful *)
-  not (pointer_eq (ctxt addsimps ths, ctxt))
-
 fun string_of_play_outcome (Played time) = string_of_ext_time (false, time)
   | string_of_play_outcome (Play_Timed_Out time) =
     if time = Time.zeroTime then "" else string_of_ext_time (true, time) ^ ", timed out"