uniformized fact selection for ATP and SMT in Sledgehammer

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Wed Feb 09 13:02:59 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Wed Feb 09 14:52:05 2022 +0100
@@ -87,6 +87,7 @@
   val bunches_of_proof_methods : Proof.context -> bool -> bool -> bool -> string ->
     proof_method list list
   val facts_of_filter : string -> (string * fact list) list -> fact list
+  val facts_of_basic_slice : base_slice -> (string * fact list) list -> fact list
   val is_fact_chained : (('a * stature) * 'b) -> bool
   val filter_used_facts : bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
     ((''a * stature) * 'b) list
@@ -238,6 +239,10 @@
     SOME facts => facts
   | NONE => snd (hd factss))
 
+fun facts_of_basic_slice (num_facts, fact_filter) factss =
+  facts_of_filter fact_filter factss
+  |> take num_facts
+
 fun is_fact_chained ((_, (sc, _)), _) = sc = Chained
 
 fun filter_used_facts keep_chained used =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Wed Feb 09 13:02:59 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Wed Feb 09 14:52:05 2022 +0100
@@ -107,12 +107,12 @@
     ({comment, state, goal, subgoal, subgoal_count, factss, found_proof} : prover_problem)
     slice =
   let
+    val (basic_slice, ATP_Slice (good_format, good_type_enc, good_lam_trans, good_uncurried_aliases, extra)) =
+      slice
+    val facts = facts_of_basic_slice basic_slice factss
     val thy = Proof.theory_of state
     val ctxt = Proof.context_of state
 
-    val ((good_max_facts, good_fact_filter), ATP_Slice (good_format, good_type_enc, good_lam_trans,
-      good_uncurried_aliases, extra)) = slice
-
     val {exec, arguments, proof_delims, known_failures, prem_role, good_max_mono_iters,
       good_max_new_mono_instances, ...} = get_atp thy name ()
 
@@ -185,16 +185,14 @@
         val type_enc = choose_type_enc strictness good_format good_type_enc
         val run_timeout = slice_timeout slices timeout
         val generous_run_timeout = if mode = MaSh then one_day else run_timeout
-        val facts = facts_of_filter good_fact_filter factss
-          |> not (is_type_enc_sound type_enc) ?
-               filter_out (is_dangerous_prop ctxt o Thm.prop_of o snd)
-          |> take good_max_facts
         val ({elapsed, ...}, atp_problem_data as (atp_problem, _, _, _)) = Timing.timing (fn () =>
           let
             val generate_info = (case good_format of DFG _ => true | _ => false)
             val readable_names = not (Config.get ctxt atp_full_names)
           in
             facts
+            |> not (is_type_enc_sound type_enc) ?
+              filter_out (is_dangerous_prop ctxt o Thm.prop_of o snd)
             |> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts
             |> map (apsnd Thm.prop_of)
             |> generate_atp_problem ctxt generate_info good_format prem_role type_enc atp_mode

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Wed Feb 09 13:02:59 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Wed Feb 09 14:52:05 2022 +0100
@@ -119,13 +119,10 @@
     ({state, goal, subgoal, subgoal_count, factss, found_proof, ...} : prover_problem)
     slice =
   let
+    val (basic_slice, SMT_Slice options) = slice
+    val facts = facts_of_basic_slice basic_slice factss
     val ctxt = Proof.context_of state
 
-    val ((good_max_facts, good_fact_filter), SMT_Slice options) = slice
-
-    val facts = facts_of_filter good_fact_filter factss
-      |> take good_max_facts
-
     val {outcome, filter_result = {fact_ids, atp_proof, ...}, used_from, run_time} =
       smt_filter name params state goal subgoal facts options
     val used_facts =