Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
changeset 62826 eb94e570c1a4
parent 62519 a564458f94db
child 69593 3dda49e08b9d 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Sat Apr 02 23:14:08 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Sat Apr 02 23:29:05 2016 +0200
@@ -52,7 +52,7 @@
 
       fun apply_f x =
         let val timeout = !next_timeout in
-          if Time.<= (timeout, min_timeout) then
+          if timeout <= min_timeout then
             NONE
           else
             let val y = f timeout x in
@@ -188,7 +188,7 @@
 
 fun add_preplay_outcomes Play_Failed _ = Play_Failed
   | add_preplay_outcomes _ Play_Failed = Play_Failed
-  | add_preplay_outcomes (Played time1) (Played time2) = Played (Time.+ (time1, time2))
+  | add_preplay_outcomes (Played time1) (Played time2) = Played (time1 + time2)
   | add_preplay_outcomes play1 play2 =
     Play_Timed_Out (Time.+ (apply2 time_of_play (play1, play2)))
isabelle