# HG changeset patch
# User blanchet
# Date 1391418858 -3600
# Node ID b9aca2f2bfeef101107e8a79b01db35e96dad6e3
# Parent  e1bf9f0c54202a79070e2e1e9a7c0960bbaae438
made SML/NJ happier

diff -r e1bf9f0c5420 -r b9aca2f2bfee src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- 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)