don't needlessly regenerate entire file when the time stamps are equal

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