src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
changeset 61666 f1b257607981
parent 61612 40859aa6d10c
child 62219 dbac573b27e7
equal deleted inserted replaced
61665:9cb2d8acf1c0 61666:f1b257607981
   213                   forced_intermediate_preplay_outcome_of_isar_step (!preplay_data))) labels of
   213                   forced_intermediate_preplay_outcome_of_isar_step (!preplay_data))) labels of
   214                 NONE => steps
   214                 NONE => steps
   215               | SOME times0 =>
   215               | SOME times0 =>
   216                 let
   216                 let
   217                   val n = length labels
   217                   val n = length labels
   218                   val total_time = Library.foldl (op Time.+) (reference_time l, times0)
   218                   val total_time = Library.foldl Time.+ (reference_time l, times0)
   219                   val timeout = adjust_merge_timeout preplay_timeout
   219                   val timeout = adjust_merge_timeout preplay_timeout
   220                     (Time.fromReal (Time.toReal total_time / Real.fromInt n))
   220                     (Time.fromReal (Time.toReal total_time / Real.fromInt n))
   221                   val meths_outcomess = @{map 2} (preplay_isar_step ctxt timeout) hopelesses succs'
   221                   val meths_outcomess = @{map 2} (preplay_isar_step ctxt timeout) hopelesses succs'
   222                 in
   222                 in
   223                   (case try (map (fn (_, Played time) :: _ => time)) meths_outcomess of
   223                   (case try (map (fn (_, Played time) :: _ => time)) meths_outcomess of