# HG changeset patch
# User wenzelm
# Date 1345716011 -7200
# Node ID 873fdafc5b0948c659755f3b10776404381fd476
# Parent  bb1f461a7815425dda173a969d4a77c661a45db1
tuned signature;

diff -r bb1f461a7815 -r 873fdafc5b09 src/Pure/ProofGeneral/pgip_isabelle.ML
--- a/src/Pure/ProofGeneral/pgip_isabelle.ML	Thu Aug 23 11:58:10 2012 +0200
+++ b/src/Pure/ProofGeneral/pgip_isabelle.ML	Thu Aug 23 12:00:11 2012 +0200
@@ -79,7 +79,7 @@
                NONE => (NONE, NONE)
              | SOME fname =>
                let val path = Path.explode fname in
-                 if can (Thy_Load.check_file Path.current) path
+                 if File.exists path
                  then (SOME (PgipTypes.pgipurl_of_path path), NONE)
                  else (NONE, SOME fname)
                end);
diff -r bb1f461a7815 -r 873fdafc5b09 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Thu Aug 23 11:58:10 2012 +0200
+++ b/src/Pure/Thy/thy_load.ML	Thu Aug 23 12:00:11 2012 +0200
@@ -9,7 +9,6 @@
   val master_directory: theory -> Path.T
   val imports_of: theory -> string list
   val provide: Path.T * SHA1.digest -> theory -> theory
-  val check_file: Path.T -> Path.T -> Path.T
   val thy_path: Path.T -> Path.T
   val check_thy: Thy_Header.keywords -> Path.T -> string ->
    {master: Path.T * SHA1.digest, text: string, imports: string list,