src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
changeset 62826 eb94e570c1a4
parent 62519 a564458f94db
child 69605 3dda49e08b9d
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Sat Apr 02 23:14:08 2016 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Sat Apr 02 23:29:05 2016 +0200
     1.3 @@ -52,7 +52,7 @@
     1.4  
     1.5        fun apply_f x =
     1.6          let val timeout = !next_timeout in
     1.7 -          if Time.<= (timeout, min_timeout) then
     1.8 +          if timeout <= min_timeout then
     1.9              NONE
    1.10            else
    1.11              let val y = f timeout x in
    1.12 @@ -188,7 +188,7 @@
    1.13  
    1.14  fun add_preplay_outcomes Play_Failed _ = Play_Failed
    1.15    | add_preplay_outcomes _ Play_Failed = Play_Failed
    1.16 -  | add_preplay_outcomes (Played time1) (Played time2) = Played (Time.+ (time1, time2))
    1.17 +  | add_preplay_outcomes (Played time1) (Played time2) = Played (time1 + time2)
    1.18    | add_preplay_outcomes play1 play2 =
    1.19      Play_Timed_Out (Time.+ (apply2 time_of_play (play1, play2)))
    1.20