get rid of minor optimization that caused strange problems and was hard to debug (and apparently saved less than 100 ms on a 30 s run)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Apr 18 10:53:27 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Apr 18 10:53:28 2012 +0200
@@ -72,7 +72,7 @@
        preplay_timeout = preplay_timeout, expect = ""}
     val problem =
       {state = state, goal = goal, subgoal = i, subgoal_count = n,
-       facts = facts, smt_filter = NONE}
+       facts = facts}
     val result as {outcome, used_facts, run_time, ...} =
       prover params (K (K (K ""))) problem
   in

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Apr 18 10:53:27 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Apr 18 10:53:28 2012 +0200
@@ -49,8 +49,7 @@
      goal: thm,
      subgoal: int,
      subgoal_count: int,
-     facts: prover_fact list,
-     smt_filter: (string * stature) SMT_Solver.smt_filter_data option}
+     facts: prover_fact list}
 
   type prover_result =
     {outcome: failure option,
@@ -314,8 +313,7 @@
    goal: thm,
    subgoal: int,
    subgoal_count: int,
-   facts: prover_fact list,
-   smt_filter: (string * stature) SMT_Solver.smt_filter_data option}
+   facts: prover_fact list}
 
 type prover_result =
   {outcome: failure option,
@@ -900,7 +898,7 @@
 fun smt_filter_loop ctxt name
                     ({debug, verbose, overlord, max_mono_iters,
                       max_new_mono_instances, timeout, slice, ...} : params)
-                    state i smt_filter =
+                    state i =
   let
     val max_slices = if slice then Config.get ctxt smt_max_slices else 1
     val repair_context =
@@ -944,9 +942,7 @@
         val _ =
           if debug then Output.urgent_message "Invoking SMT solver..." else ()
         val (outcome, used_facts) =
-          (case (slice, smt_filter) of
-             (1, SOME head) => head |> apsnd (apsnd repair_context)
-           | _ => SMT_Solver.smt_filter_preprocess state facts i)
+          SMT_Solver.smt_filter_preprocess state facts i
           |> SMT_Solver.smt_filter_apply slice_timeout
           |> (fn {outcome, used_facts} => (outcome, used_facts))
           handle exn => if Exn.is_interrupt exn then
@@ -995,15 +991,14 @@
 
 fun run_smt_solver mode name (params as {debug, verbose, preplay_timeout, ...})
         minimize_command
-        ({state, subgoal, subgoal_count, facts, smt_filter, ...}
-         : prover_problem) =
+        ({state, subgoal, subgoal_count, facts, ...} : prover_problem) =
   let
     val ctxt = Proof.context_of state
     val num_facts = length facts
     val facts = facts ~~ (0 upto num_facts - 1)
                 |> map (smt_weighted_fact ctxt num_facts)
     val {outcome, used_facts = used_pairs, run_time} =
-      smt_filter_loop ctxt name params state subgoal smt_filter facts
+      smt_filter_loop ctxt name params state subgoal facts
     val used_facts = used_pairs |> map fst
     val outcome = outcome |> Option.map failure_from_smt_failure
     val (preplay, message, message_tail) =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Apr 18 10:53:27 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Apr 18 10:53:28 2012 +0200
@@ -177,8 +177,8 @@
 
 fun launch_prover (params as {debug, verbose, blocking, max_relevant, slice,
                               timeout, expect, ...})
-        mode minimize_command only
-        {state, goal, subgoal, subgoal_count, facts, smt_filter} name =
+        mode minimize_command only {state, goal, subgoal, subgoal_count, facts}
+        name =
   let
     val ctxt = Proof.context_of state
     val hard_timeout = Time.+ (timeout, timeout)
@@ -197,8 +197,7 @@
          subgoal_count = subgoal_count, facts =
           ((Sledgehammer_Provers.is_ho_atp ctxt name |> not) ? filter_induction)
             facts
-          |> take num_facts,
-         smt_filter = smt_filter}
+          |> take num_facts}
       end
     fun really_go () =
       problem
@@ -268,14 +267,11 @@
   ctxt |> select_smt_solver name
        |> SMT_Config.solver_class_of |> SMT_Utils.string_of_class
 
-fun dest_SMT_Weighted_Fact (SMT_Weighted_Fact p) = p
-  | dest_SMT_Weighted_Fact _ = raise Fail "dest_SMT_Weighted_Fact"
-
 val auto_try_max_relevant_divisor = 2 (* FUDGE *)
 
 fun run_sledgehammer (params as {debug, verbose, blocking, provers,
                                  relevance_thresholds, max_relevant, slice,
-                                 timeout, ...})
+                                 ...})
         mode i (relevance_override as {only, ...}) minimize_command state =
   if null provers then
     error "No prover is set."
@@ -303,7 +299,7 @@
       val (smts, (ueq_atps, full_atps)) =
         provers |> List.partition (is_smt_prover ctxt)
                 ||> List.partition (is_unit_equational_atp ctxt)
-      fun launch_provers state get_facts translate maybe_smt_filter provers =
+      fun launch_provers state get_facts translate provers =
         let
           val facts = get_facts ()
           val num_facts = length facts
@@ -311,9 +307,7 @@
                       |> map (translate num_facts)
           val problem =
             {state = state, goal = goal, subgoal = i, subgoal_count = n,
-             facts = facts,
-             smt_filter = maybe_smt_filter
-                  (fn () => map_filter (try dest_SMT_Weighted_Fact) facts) i}
+             facts = facts}
           val launch = launch_prover params mode minimize_command only
         in
           if mode = Auto_Try orelse mode = Try then
@@ -377,7 +371,7 @@
         else
           launch_provers state
               (get_facts label is_appropriate_prop atp_relevance_fudge o K atps)
-              (K (Untranslated_Fact o fst)) (K (K NONE)) atps
+              (K (Untranslated_Fact o fst)) atps
       fun launch_smts accum =
         if null smts then
           accum
@@ -385,15 +379,10 @@
           let
             val facts = get_facts "SMT solver" NONE smt_relevance_fudge smts
             val weight = SMT_Weighted_Fact oo weight_smt_fact ctxt
-            fun smt_filter facts =
-              (if debug then curry (op o) SOME
-               else TimeLimit.timeLimit timeout o try)
-                  (SMT_Solver.smt_filter_preprocess state (facts ()))
           in
             smts |> map (`(class_of_smt_solver ctxt))
                  |> AList.group (op =)
-                 |> map (snd #> launch_provers state (K facts) weight smt_filter
-                             #> fst)
+                 |> map (snd #> launch_provers state (K facts) weight #> fst)
                  |> max_outcome_code |> rpair state
           end
       val launch_full_atps = launch_atps "ATP" NONE full_atps