# HG changeset patch
# User blanchet
# Date 1391370831 -3600
# Node ID 235205726737eaf40572a66826e339434e9d78fd
# Parent  4aa3e1c6222c5a15f78e4b85def0451b97238e60
made SML/NJ happier

diff -r 4aa3e1c6222c -r 235205726737 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Sun Feb 02 20:53:51 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Sun Feb 02 20:53:51 2014 +0100
@@ -191,13 +191,11 @@
         (* 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 f slices = fold (Integer.max o fst o #1 o fst o snd o f) slices 0
+        fun max_facts_of_slices slices = 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 I all_slices
-            | SOME max => max)
-          / Real.fromInt (max_facts_of_slices snd actual_slices)
+          Real.fromInt (case max_facts of NONE => max_facts_of_slices all_slices | SOME max => max)
+          / Real.fromInt (max_facts_of_slices (map snd actual_slices))
 
         fun monomorphize_facts facts =
           let