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,