1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jul 24 18:53:14 2014 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jul 24 19:01:06 2014 +0200
     1.3 @@ -699,7 +699,7 @@
     1.4        val dirty_facts' =
     1.5          (case try OS.FileSys.modTime (Path.implode path) of
     1.6            NONE => NONE
     1.7 -        | SOME disk_time => if Time.< (disk_time, memory_time) then dirty_facts else NONE)
     1.8 +        | SOME disk_time => if Time.<= (disk_time, memory_time) then dirty_facts else NONE)
     1.9        val (banner, entries) =
    1.10          (case dirty_facts' of
    1.11            SOME names => (NONE, fold (append_entry o Graph.get_entry access_G) names [])