# HG changeset patch
# User blanchet
# Date 1381965008 -7200
# Node ID 6675cdc0d1ae524ba6a8932eeb99b51087ab4f7b
# Parent  420b876ff1e2df1a63f691bbfd91976f3ed55b20
if slicing is disabled, pick the maximum number of facts, not the number of facts in the last slice

diff -r 420b876ff1e2 -r 6675cdc0d1ae src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Oct 17 01:04:00 2013 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Oct 17 01:10:08 2013 +0200
@@ -454,8 +454,7 @@
           |> sh_minimizeLST (*don't confuse the two minimization flags*)
           |> max_new_mono_instancesLST
           |> max_mono_itersLST)
-    val default_max_facts =
-      Sledgehammer_Provers.default_max_facts_of_prover ctxt slice prover_name
+    val default_max_facts = Sledgehammer_Provers.default_max_facts_of_prover ctxt prover_name
     val is_appropriate_prop =
       Sledgehammer_Provers.is_appropriate_prop_of_prover ctxt prover_name
     val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt
diff -r 420b876ff1e2 -r 6675cdc0d1ae src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Thu Oct 17 01:04:00 2013 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Thu Oct 17 01:10:08 2013 +0200
@@ -113,8 +113,7 @@
          val prover = AList.lookup (op =) args "prover" |> the_default default_prover
          val params as {max_facts, slice, ...} =
            Sledgehammer_Isar.default_params ctxt args
-         val default_max_facts =
-           Sledgehammer_Provers.default_max_facts_of_prover ctxt slice prover
+         val default_max_facts = Sledgehammer_Provers.default_max_facts_of_prover ctxt prover
          val is_appropriate_prop =
            Sledgehammer_Provers.is_appropriate_prop_of_prover ctxt default_prover
          val relevance_fudge =
diff -r 420b876ff1e2 -r 6675cdc0d1ae src/HOL/TPTP/sledgehammer_tactics.ML
--- a/src/HOL/TPTP/sledgehammer_tactics.ML	Thu Oct 17 01:04:00 2013 +0200
+++ b/src/HOL/TPTP/sledgehammer_tactics.ML	Thu Oct 17 01:10:08 2013 +0200
@@ -27,18 +27,16 @@
 fun run_prover override_params fact_override i n ctxt goal =
   let
     val mode = Normal
-    val params as {provers, max_facts, slice, ...} =
-      default_params ctxt override_params
+    val params as {provers, max_facts, ...} = default_params ctxt override_params
     val name = hd provers
     val prover = get_prover ctxt mode name
-    val default_max_facts = default_max_facts_of_prover ctxt slice name
+    val default_max_facts = default_max_facts_of_prover ctxt name
     val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt
     val ho_atp = exists (is_ho_atp ctxt) provers
     val reserved = reserved_isar_keyword_table ()
     val css_table = clasimpset_rule_table_of ctxt
     val facts =
-      nearly_all_facts ctxt ho_atp fact_override reserved css_table [] hyp_ts
-                       concl_t
+      nearly_all_facts ctxt ho_atp fact_override reserved css_table [] hyp_ts concl_t
       |> relevant_facts ctxt params name
              (the_default default_max_facts max_facts) fact_override hyp_ts
              concl_t
diff -r 420b876ff1e2 -r 6675cdc0d1ae src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Oct 17 01:04:00 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Oct 17 01:10:08 2013 +0200
@@ -96,7 +96,7 @@
     Proof.context -> string -> string option
   val remotify_prover_if_not_installed :
     Proof.context -> string -> string option
-  val default_max_facts_of_prover : Proof.context -> bool -> string -> int
+  val default_max_facts_of_prover : Proof.context -> string -> int
   val is_unit_equality : term -> bool
   val is_appropriate_prop_of_prover : Proof.context -> string -> term -> bool
   val weight_smt_fact :
@@ -207,13 +207,12 @@
 
 fun slice_max_facts (_, ( ((max_facts, _), _, _, _, _), _)) = max_facts
 
-fun default_max_facts_of_prover ctxt slice name =
+fun default_max_facts_of_prover ctxt name =
   let val thy = Proof_Context.theory_of ctxt in
     if is_reconstructor name then
       reconstructor_default_max_facts
     else if is_atp thy name then
-      fold (Integer.max o slice_max_facts o snd)
-           (get_slices slice (#best_slices (get_atp thy name ()) ctxt)) 0
+      fold (Integer.max o slice_max_facts) (#best_slices (get_atp thy name ()) ctxt) 0
     else (* is_smt_prover ctxt name *)
       SMT_Solver.default_max_relevant ctxt name
   end
diff -r 420b876ff1e2 -r 6675cdc0d1ae src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Oct 17 01:04:00 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Oct 17 01:10:08 2013 +0200
@@ -76,7 +76,7 @@
     val _ = spying spy (fn () => (state, subgoal, name, "Launched"));
     val birth_time = Time.now ()
     val death_time = Time.+ (birth_time, hard_timeout)
-    val max_facts = max_facts |> the_default (default_max_facts_of_prover ctxt slice name)
+    val max_facts = max_facts |> the_default (default_max_facts_of_prover ctxt name)
     val num_facts = length facts |> not only ? Integer.min max_facts
 
     fun desc () = prover_description ctxt params name num_facts subgoal subgoal_count goal
@@ -257,8 +257,7 @@
             case max_facts of
               SOME n => n
             | NONE =>
-              0 |> fold (Integer.max o default_max_facts_of_prover ctxt slice)
-                        provers
+              0 |> fold (Integer.max o default_max_facts_of_prover ctxt) provers
                 |> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor)
           val _ = spying spy (fn () => (state, i, label ^ "s",
             "Filtering " ^ string_of_int (length all_facts) ^ " facts"));