# 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)