src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML

     | _ => NONE)
   | _ => NONE)
 
 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
         time_state
       else

       fun append_entry (name, ((kind, feats, deps), (parents, _))) =
         cons (kind, name, Graph.Keys.dest parents, feats, deps)
 
       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) =
         (case dirty_facts' of
           SOME names => (NONE, fold (append_entry o Graph.get_entry access_G) names [])