# HG changeset patch
# User wenzelm
# Date 1206997731 -7200
# Node ID 494f418cc51c65206aab0728b36125a13400b886
# Parent  b4f0f36a28daf7ba281c6b6349a6eb9b17d927a4
discontinued File.explode_platform_path -- use plain Path.explode;

diff -r b4f0f36a28da -r 494f418cc51c src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Sun Mar 30 23:17:55 2008 +0200
+++ b/src/HOL/Tools/res_atp.ML	Mon Mar 31 23:08:51 2008 +0200
@@ -97,13 +97,13 @@
       "" => error  ("Isabelle environment variable " ^ evar ^ " not defined")
     | home =>
         let val path = home ^ "/" ^ base
-        in  if File.exists (File.explode_platform_path path) then path
+        in  if File.exists (Path.explode path) then path
             else error ("Could not find the file " ^ path)
         end;
 
 fun probfile_nosuffix _ =
   if !destdir = "" then File.platform_path (File.tmp_path (Path.basic (!problem_name)))
-  else if File.exists (File.explode_platform_path (!destdir))
+  else if File.exists (Path.explode (!destdir))
   then !destdir ^ "/" ^ !problem_name
   else error ("No such directory: " ^ !destdir);
 
@@ -113,7 +113,7 @@
     let val file = !problem_name
     in
         if !destdir = "" then File.platform_path (File.tmp_path (Path.basic file))
-        else if File.exists (File.explode_platform_path (!destdir))
+        else if File.exists (Path.explode (!destdir))
         then !destdir ^ "/" ^ file
         else error ("No such directory: " ^ !destdir)
     end;
@@ -717,7 +717,7 @@
 
 (*For debugging the generated set of theorem names*)
 fun trace_vector fname =
-  let val path = File.explode_platform_path (fname ^ "_thm_names")
+  let val path = Path.explode (fname ^ "_thm_names")
   in  Vector.app (File.append path o (fn s => s ^ "\n"))  end;
 
 (*We write out problem files for each subgoal. Argument probfile generates filenames,