src/HOL/Tools/Sledgehammer/sledgehammer_run.ML

 fun is_induction_fact (Untranslated_Fact ((_, (_, Induction)), _)) = true
   | is_induction_fact _ = false
 
 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)
     val birth_time = Time.now ()
     val death_time = Time.+ (birth_time, hard_timeout)

         val filter_induction = filter_out is_induction_fact
       in {state = state, goal = goal, subgoal = subgoal,
          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
       |> get_minimizing_prover ctxt mode name params minimize_command
       |> (fn {outcome, preplay, message, message_tail, ...} =>

 
 fun class_of_smt_solver ctxt name =
   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."
   else case subgoal_count state of
     0 => (Output.urgent_message "No subgoal!"; (false, (noneN, state)))

               | NONE => ()
       val _ = print "Sledgehammering..."
       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
           val facts = facts ~~ (0 upto num_facts - 1)
                       |> 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
             (unknownN, state)
             |> fold (fn prover => fn accum as (outcome_code, _) =>

              ();
            accum)
         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
         else
           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
       val launch_ueq_atps =
         launch_atps "Unit equational provers" (SOME is_unit_equality) ueq_atps