--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Feb 03 10:14:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Feb 03 10:14:18 2014 +0100
@@ -187,7 +187,10 @@
(* If slicing is disabled, we expand the last slice to fill the entire time available. *)
val all_slices = best_slices ctxt
val actual_slices = get_slices slice all_slices
- fun max_facts_of_slices slices = fold (Integer.max o fst o #1 o fst o snd) slices 0
+
+ fun max_facts_of_slices (slices : (real * (slice_spec * string)) list) =
+ fold (Integer.max o fst o #1 o fst o snd) slices 0
+
val num_actual_slices = length actual_slices
val max_fact_factor =
Real.fromInt (case max_facts of NONE => max_facts_of_slices all_slices | SOME max => max)