# HG changeset patch
# User wenzelm
# Date 1184879935 -7200
# Node ID c886d989723748498134aa781c364971d0571b0d
# Parent  8c6f2e7bfdb4734526b712826b5169de8b9c82b4
adapted ThyLoad.deps_thy

diff -r 8c6f2e7bfdb4 -r c886d9897237 src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Jul 19 23:18:55 2007 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Jul 19 23:18:55 2007 +0200
@@ -692,15 +692,14 @@
 
         fun filerefs f =
             let val thy = thy_name f
-                val (_,filerefs) = OuterSyntax.deps_thy thy true f (* (Path.unpack f); *)
+                val (_, (_,filerefs)) = ThyLoad.deps_thy [Path.dir f] thy true
             in
                 issue_pgip (Setrefs {url=url, thyname=NONE, objtype=SOME PgipTypes.ObjFile,
                                      name=NONE, idtables=[], fileurls=filerefs})
             end
 
         fun thyrefs thy =
-            let val ml_path = ThyLoad.ml_path thy
-                val (thyrefs,_) = OuterSyntax.deps_thy thy true ml_path (* (Path.unpack f); *)
+            let val (_, (thyrefs,_)) = ThyLoad.deps_thy [] thy true
             in
                 issue_pgip (Setrefs {url=url, thyname=thyname, objtype=SOME PgipTypes.ObjTheory,
                                      name=NONE, idtables=[{context=NONE, objtype=PgipTypes.ObjTheory,