discontinued File.explode_platform_path -- use plain Path.explode;
authorwenzelm
Mon Mar 31 23:08:51 2008 +0200 (2008-03-31)
changeset 26501494f418cc51c
parent 26500 b4f0f36a28da
child 26502 7f64d8cf6707
discontinued File.explode_platform_path -- use plain Path.explode;
src/HOL/Tools/res_atp.ML
     1.1 --- a/src/HOL/Tools/res_atp.ML	Sun Mar 30 23:17:55 2008 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Mon Mar 31 23:08:51 2008 +0200
     1.3 @@ -97,13 +97,13 @@
     1.4        "" => error  ("Isabelle environment variable " ^ evar ^ " not defined")
     1.5      | home =>
     1.6          let val path = home ^ "/" ^ base
     1.7 -        in  if File.exists (File.explode_platform_path path) then path
     1.8 +        in  if File.exists (Path.explode path) then path
     1.9              else error ("Could not find the file " ^ path)
    1.10          end;
    1.11  
    1.12  fun probfile_nosuffix _ =
    1.13    if !destdir = "" then File.platform_path (File.tmp_path (Path.basic (!problem_name)))
    1.14 -  else if File.exists (File.explode_platform_path (!destdir))
    1.15 +  else if File.exists (Path.explode (!destdir))
    1.16    then !destdir ^ "/" ^ !problem_name
    1.17    else error ("No such directory: " ^ !destdir);
    1.18  
    1.19 @@ -113,7 +113,7 @@
    1.20      let val file = !problem_name
    1.21      in
    1.22          if !destdir = "" then File.platform_path (File.tmp_path (Path.basic file))
    1.23 -        else if File.exists (File.explode_platform_path (!destdir))
    1.24 +        else if File.exists (Path.explode (!destdir))
    1.25          then !destdir ^ "/" ^ file
    1.26          else error ("No such directory: " ^ !destdir)
    1.27      end;
    1.28 @@ -717,7 +717,7 @@
    1.29  
    1.30  (*For debugging the generated set of theorem names*)
    1.31  fun trace_vector fname =
    1.32 -  let val path = File.explode_platform_path (fname ^ "_thm_names")
    1.33 +  let val path = Path.explode (fname ^ "_thm_names")
    1.34    in  Vector.app (File.append path o (fn s => s ^ "\n"))  end;
    1.35  
    1.36  (*We write out problem files for each subgoal. Argument probfile generates filenames,