# HG changeset patch
# User blanchet
# Date 1381964640 -7200
# Node ID 420b876ff1e2df1a63f691bbfd91976f3ed55b20
# Parent  d3c0cf737b55be5fcb8ea25beef40062f8f9c487
if slicing is disabled, don't enforce last slice's "max_facts", but rather the maximum "max_facts"

diff -r d3c0cf737b55 -r 420b876ff1e2 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Oct 17 01:03:59 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Oct 17 01:04:00 2013 +0200
@@ -704,7 +704,7 @@
    isn't much to learn from such proofs. *)
 val max_dependencies = 20
 
-val prover_default_max_facts = 50
+val prover_default_max_facts = 25
 
 (* "type_definition_xxx" facts are characterized by their use of "CollectI". *)
 val typedef_dep = nickname_of_thm @{thm CollectI}
diff -r d3c0cf737b55 -r 420b876ff1e2 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Oct 17 01:03:59 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Oct 17 01:04:00 2013 +0200
@@ -205,14 +205,14 @@
 
 val reconstructor_default_max_facts = 20
 
-fun slice_max_facts (_, (_, ( ((max_facts, _), _, _, _, _), _))) = max_facts
+fun slice_max_facts (_, ( ((max_facts, _), _, _, _, _), _)) = max_facts
 
 fun default_max_facts_of_prover ctxt slice 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)
+      fold (Integer.max o slice_max_facts o snd)
            (get_slices slice (#best_slices (get_atp thy name ()) ctxt)) 0
     else (* is_smt_prover ctxt name *)
       SMT_Solver.default_max_relevant ctxt name
@@ -617,15 +617,15 @@
       let
         (* If slicing is disabled, we expand the last slice to fill the entire
            time available. *)
-        val actual_slices = get_slices slice (best_slices ctxt)
+        val all_slices = best_slices ctxt
+        val actual_slices = get_slices slice all_slices
+        fun max_facts_of_slices f slices = fold (Integer.max o slice_max_facts o f) slices 0
         val num_actual_slices = length actual_slices
         val max_fact_factor =
-          case max_facts of
-            NONE => 1.0
-          | SOME max =>
-            Real.fromInt max
-            / Real.fromInt (fold (Integer.max o slice_max_facts)
-                                 actual_slices 0)
+          Real.fromInt (case max_facts of
+              NONE => max_facts_of_slices I all_slices
+            | SOME max => max)
+          / Real.fromInt (max_facts_of_slices snd actual_slices)
         fun monomorphize_facts facts =
           let
             val ctxt =