src/HOL/Tools/res_atp.ML
changeset 21858 05f57309170c
parent 21790 9d2761d09d91
child 21888 c75a44597fb7
     1.1 --- a/src/HOL/Tools/res_atp.ML	Thu Dec 14 22:19:39 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Dec 15 00:08:06 2006 +0100
     1.3 @@ -99,13 +99,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.unpack_platform_path path) then path
     1.8 +        in  if File.exists (File.explode_platform_path 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.unpack_platform_path (!destdir))
    1.15 +  else if File.exists (File.explode_platform_path (!destdir))
    1.16    then !destdir ^ "/" ^ !problem_name
    1.17    else error ("No such directory: " ^ !destdir);
    1.18  
    1.19 @@ -149,7 +149,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.unpack_platform_path (!destdir))
    1.24 +        else if File.exists (File.explode_platform_path (!destdir))
    1.25          then !destdir ^ "/" ^ file
    1.26          else error ("No such directory: " ^ !destdir)
    1.27      end;
    1.28 @@ -463,7 +463,7 @@
    1.29  (*Reject theorems with names like "List.filter.filter_list_def" or
    1.30    "Accessible_Part.acc.defs", as these are definitions arising from packages.*)
    1.31  fun is_package_def a =
    1.32 -  let val names = NameSpace.unpack a
    1.33 +  let val names = NameSpace.explode a
    1.34    in
    1.35       length names > 2 andalso
    1.36       not (hd names = "local") andalso
    1.37 @@ -820,7 +820,7 @@
    1.38    end
    1.39  
    1.40  fun trace_array fname =
    1.41 -  let val path = File.unpack_platform_path fname
    1.42 +  let val path = File.explode_platform_path fname
    1.43    in  Array.app (File.append path o (fn s => s ^ "\n"))  end;
    1.44  
    1.45  (*Converting a subgoal into negated conjecture clauses*)