src/Pure/ProofGeneral/proof_general_pgip.ML
changeset 48927 ef462b5558eb
parent 48898 9fc880720663
child 50201 c26369c9eda6
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Aug 26 10:20:26 2012 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Aug 26 21:46:50 2012 +0200
@@ -601,7 +601,7 @@
             end
 
         fun thyrefs thy =
-            let val thyrefs = #imports (Thy_Load.check_thy Path.current thy)
+            let val thyrefs = map #1 (#imports (Thy_Load.check_thy Path.current thy))
             in
                 issue_pgip (Setrefs {url=url, thyname=thyname, objtype=SOME PgipTypes.ObjTheory,
                                      name=NONE, idtables=[{context=NONE, objtype=PgipTypes.ObjTheory,