# HG changeset patch
# User blanchet
# Date 1406221266 -7200
# Node ID cffd1d6ae1e5ccce7bf7c3871f447faa7d625961
# Parent  1586d0479f2c6937cd7a7c4671e9b81c3ecf3dca
don't needlessly regenerate entire file when the time stamps are equal

diff -r 1586d0479f2c -r cffd1d6ae1e5 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- 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 [])