# HG changeset patch
# User wenzelm
# Date 1439909372 -7200
# Node ID 6dfe08f5834ec26db3a8436e38e55bc8119ff1d8
# Parent  e08d868ceca9a12a7a71d6ede3bb4939118eb38f
proper platform_path;

diff -r e08d868ceca9 -r 6dfe08f5834e src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Aug 18 16:08:47 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Aug 18 16:49:32 2015 +0200
@@ -653,7 +653,7 @@
 
 fun load_state ctxt (time_state as (memory_time, _)) =
   let val path = state_file () in
-    (case try OS.FileSys.modTime (Path.implode path) of
+    (case try OS.FileSys.modTime (File.platform_path path) of
       NONE => time_state
     | SOME disk_time =>
       if Time.>= (memory_time, disk_time) then
@@ -699,7 +699,7 @@
 
       val path = state_file ()
       val dirty_facts' =
-        (case try OS.FileSys.modTime (Path.implode path) of
+        (case try OS.FileSys.modTime (File.platform_path path) of
           NONE => NONE
         | SOME disk_time => if Time.<= (disk_time, memory_time) then dirty_facts else NONE)
       val (banner, entries) =