made SML/NJ happier
authorblanchet
Sun Feb 02 20:53:51 2014 +0100 (2014-02-02)
changeset 55248235205726737
parent 55247 4aa3e1c6222c
child 55249 0ff946f0b764
made SML/NJ happier
src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Sun Feb 02 20:53:51 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Sun Feb 02 20:53:51 2014 +0100
     1.3 @@ -191,13 +191,11 @@
     1.4          (* If slicing is disabled, we expand the last slice to fill the entire time available. *)
     1.5          val all_slices = best_slices ctxt
     1.6          val actual_slices = get_slices slice all_slices
     1.7 -        fun max_facts_of_slices f slices = fold (Integer.max o fst o #1 o fst o snd o f) slices 0
     1.8 +        fun max_facts_of_slices slices = fold (Integer.max o fst o #1 o fst o snd) slices 0
     1.9          val num_actual_slices = length actual_slices
    1.10          val max_fact_factor =
    1.11 -          Real.fromInt (case max_facts of
    1.12 -              NONE => max_facts_of_slices I all_slices
    1.13 -            | SOME max => max)
    1.14 -          / Real.fromInt (max_facts_of_slices snd actual_slices)
    1.15 +          Real.fromInt (case max_facts of NONE => max_facts_of_slices all_slices | SOME max => max)
    1.16 +          / Real.fromInt (max_facts_of_slices (map snd actual_slices))
    1.17  
    1.18          fun monomorphize_facts facts =
    1.19            let