# HG changeset patch
# User wenzelm
# Date 1185741720 -7200
# Node ID 69b51bc5ce06f126404ed069a3863d961cc822c6
# Parent  fb455cb475df9e95c5eef83080c552e1e4e3330e
adapted ThyLoad.deps_thy;

diff -r fb455cb475df -r 69b51bc5ce06 src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Jul 29 22:41:59 2007 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Jul 29 22:42:00 2007 +0200
@@ -692,14 +692,14 @@
 
         fun filerefs f =
             let val thy = thy_name f
-                val (_, (_,filerefs)) = ThyLoad.deps_thy (Path.dir f) thy true
+                val filerefs = #uses (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 (_, (thyrefs,_)) = ThyLoad.deps_thy Path.current thy true
+            let val thyrefs = #imports (ThyLoad.deps_thy Path.current thy true)
             in
                 issue_pgip (Setrefs {url=url, thyname=thyname, objtype=SOME PgipTypes.ObjTheory,
                                      name=NONE, idtables=[{context=NONE, objtype=PgipTypes.ObjTheory,